[Merged by Bors] - feat(Algebra/MvPolynomial/Basic): `coeff_C_of_ne_zero` and `coeff_add_single_C` by justus-springer · Pull Request #39623 · leanprover-community/mathlib4

justus-springer · 2026-05-20T16:51:05Z

These lemmas are multivariate analogs to Polynomial.coeff_C_of_ne_zero, Polynomial.coeff_C_succ and PowerSeries.coeff_C_of_ne_zero and PowerSeries.coeff_succ_C. They are useful for defining partial derivatives for multivariate power series, see PR #39626.

depends on: [Merged by Bors] - chore: fix naming of coeff_C_ne_zero #39632

github-actions · 2026-05-20T16:52:25Z

PR summary dde92fab4e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

++ coeff_C_of_ne_zero
++ coeff_add_single_C

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit dde92fa).

+4 new declarations
−0 removed declarations

+MvPolynomial.coeff_C_of_ne_zero
+MvPolynomial.coeff_add_single_C
+MvPowerSeries.coeff_C_of_ne_zero
+MvPowerSeries.coeff_add_single_C

No changes to strong technical debt.

No changes to weak technical debt.

Current commit dde92fab4e
Reference commit fa97836994

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

wwylele · 2026-05-20T19:42:17Z

It looks like there is build failure due to the rename of existing lemma. I suggest putting the rename in a separate PR

justus-springer · 2026-05-20T20:47:50Z

Yes, this occurrence must have slipped through. I've split off the renaming as #39632.

Split off from #39623

mathlib-dependent-issues · 2026-05-20T22:44:18Z

This PR/issue depends on:

~~[Merged by Bors] - chore: fix naming of coeff_C_ne_zero #39632~~
By Dependent Issues (🤖). Happy coding!

Split off from leanprover-community#39623

Hagb

Maybe with NeZero so that it can simplify cases with other positive literals? I am not sure whether it is a good practice here though.

Co-authored-by: Hagb (Junyu Guo 郭俊余) <hagbgreen@yahoo.com>

Split off from leanprover-community#39623

faenuccio · 2026-06-20T14:27:06Z

@justus-springer Can you update master here as well? Thanks

justus-springer · 2026-06-22T11:07:12Z

@faenuccio I updated master, no changes were necessary. Is this mergeable soon?

Co-authored-by: Noah Walker <noahwalker3.14@gmail.com>

tb65536

Thanks!

maintainer merge

github-actions · 2026-06-23T13:12:13Z

🚀 Pull request has been placed on the maintainer queue by tb65536.

riccardobrasca

Thanks!

bors d+

mathlib-bors · 2026-06-23T13:14:51Z

✌️ justus-springer can now approve this pull request until 2026-07-07 13:14 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

…om/justus-springer/mathlib4 into justus/MvPolynomial_coeff_C_lemmas

justus-springer · 2026-06-24T10:06:19Z

bors r+

…_single_C` (#39623) These lemmas are multivariate analogs to `Polynomial.coeff_C_of_ne_zero`, `Polynomial.coeff_C_succ` and `PowerSeries.coeff_C_of_ne_zero` and `PowerSeries.coeff_succ_C`. They are useful for defining partial derivatives for multivariate power series, see PR #39626. - [x] depends on: #39632

mathlib-bors · 2026-06-24T11:46:32Z

Pull request successfully merged into master.

Build succeeded:

#39626) Previously, we had formal derivatives for `PowerSeries` and `Polynomial` and formal partial derivatives for `MvPolynomial`, but no formal partial derivatives for `MvPowerSeries`. This PR adds them. Furthermore, `PowerSeries.derivative` is refactored to be defined in terms of `MvPowerSeries.pderiv`, which reduces code duplication (In particular, there is no need to define the bare function `PowerSeries.derivativeFun` anymore). Most proofs are direct generalizations from the univariate case. I only had to add a few missing API lemmas, which I am PR'ing separately below: - [x] depends on: #39623 - [x] depends on: #39624 - [x] depends on: #39625

add lemmas

36def95

github-actions Bot added the t-ring-theory Ring theory label May 20, 2026

justus-springer mentioned this pull request May 20, 2026

[Merged by Bors] - feat(RingTheory/MvPowerSeries): partial derivatives of MvPowerSeries #39626

Closed

3 tasks

wwylele reviewed May 20, 2026

View reviewed changes

Comment thread Mathlib/Algebra/MvPolynomial/Basic.lean Outdated

rename

7d5a50b

fix

9cf5760

justus-springer mentioned this pull request May 20, 2026

[Merged by Bors] - chore: fix naming of coeff_C_ne_zero #39632

Closed

wwylele approved these changes May 20, 2026

View reviewed changes

mathlib-bors Bot pushed a commit that referenced this pull request May 20, 2026

chore: fix naming of coeff_C_ne_zero (#39632)

ae5f1c0

Split off from #39623

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 20, 2026

Merge branch 'master' into justus/MvPolynomial_coeff_C_lemmas

fc46ae0

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 20, 2026

justus-springer changed the title ~~feat(Algebra/MvPolynomial/Basic): coeff_ne_zero_C and coeff_add_single_C~~ feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and coeff_add_single_C May 20, 2026

RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 22, 2026

chore: fix naming of coeff_C_ne_zero (leanprover-community#39632)

664bb1c

Split off from leanprover-community#39623

Hagb approved these changes May 24, 2026

View reviewed changes

Comment thread Mathlib/Algebra/MvPolynomial/Basic.lean Outdated

Hagb reviewed May 24, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/MvPowerSeries/Basic.lean Outdated

justus-springer and others added 2 commits May 25, 2026 09:28

Update Mathlib/Algebra/MvPolynomial/Basic.lean

80df352

Co-authored-by: Hagb (Junyu Guo 郭俊余) <hagbgreen@yahoo.com>

Update Mathlib/RingTheory/MvPowerSeries/Basic.lean

0903d12

Co-authored-by: Hagb (Junyu Guo 郭俊余) <hagbgreen@yahoo.com>

b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026

chore: fix naming of coeff_C_ne_zero (leanprover-community#39632)

a83e92a

Split off from leanprover-community#39623

Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026

chore: fix naming of coeff_C_ne_zero (leanprover-community#39632)

545fbb6

Split off from leanprover-community#39623

mathlib-triage Bot assigned faenuccio Jun 19, 2026

tb65536 reviewed Jun 19, 2026

View reviewed changes

Comment thread Mathlib/Algebra/MvPolynomial/Basic.lean Outdated

justus-springer added 2 commits June 20, 2026 16:49

add comments

97c39e4

Merge branch 'master' into justus/MvPolynomial_coeff_C_lemmas

140197e

justus-springer added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 20, 2026

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 20, 2026

NoahW314 reviewed Jun 22, 2026

View reviewed changes

Comment thread Mathlib/Algebra/MvPolynomial/Basic.lean Outdated

Comment thread Mathlib/RingTheory/MvPowerSeries/Basic.lean Outdated

Apply suggestions from code review

9eb370c

Co-authored-by: Noah Walker <noahwalker3.14@gmail.com>

tb65536 approved these changes Jun 23, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 23, 2026

riccardobrasca reviewed Jun 23, 2026

View reviewed changes

Comment thread Mathlib/Algebra/MvPolynomial/Basic.lean Outdated

Comment thread Mathlib/RingTheory/MvPowerSeries/Basic.lean Outdated

mathlib-triage Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 23, 2026

justus-springer added 3 commits June 24, 2026 08:33

make arguments explicit

ec2236b

Merge branch 'master' into justus/MvPolynomial_coeff_C_lemmas

fb74954

Merge branch 'justus/MvPolynomial_coeff_C_lemmas' of https://github.c…

52e8dfa

…om/justus-springer/mathlib4 into justus/MvPolynomial_coeff_C_lemmas

justus-springer added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 24, 2026

fix

dde92fa

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 24, 2026

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jun 24, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jun 24, 2026

mathlib-bors Bot changed the title ~~feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and coeff_add_single_C~~ [Merged by Bors] - feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and coeff_add_single_C Jun 24, 2026

mathlib-bors Bot closed this Jun 24, 2026

mathlib-bors Bot removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jun 24, 2026

Uh oh!

Conversation

justus-springer commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary dde92fab4e

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

wwylele commented May 20, 2026

Uh oh!

justus-springer commented May 20, 2026

Uh oh!

mathlib-dependent-issues Bot commented May 20, 2026

Uh oh!

Hagb left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

faenuccio commented Jun 20, 2026

Uh oh!

justus-springer commented Jun 22, 2026

Uh oh!

Uh oh!

Uh oh!

tb65536 left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Jun 23, 2026

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors Bot commented Jun 23, 2026

Uh oh!

justus-springer commented Jun 24, 2026

Uh oh!

mathlib-bors Bot commented Jun 24, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

justus-springer commented May 20, 2026 •

edited

Loading

github-actions Bot commented May 20, 2026 •

edited

Loading

Hagb left a comment •

edited

Loading