Skip to content

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

Closed
justus-springer wants to merge 2 commits into
leanprover-community:masterfrom
justus-springer:justus/MvPolynomial_coeff_C_fix_naming
Closed

[Merged by Bors] - chore: fix naming of coeff_C_ne_zero#39632
justus-springer wants to merge 2 commits into
leanprover-community:masterfrom
justus-springer:justus/MvPolynomial_coeff_C_fix_naming

Conversation

@justus-springer

@justus-springer justus-springer commented May 20, 2026

Copy link
Copy Markdown
Collaborator

Split off from #39623

Open in Gitpod

@justus-springer justus-springer mentioned this pull request May 20, 2026
Closed
1 task
@github-actions

github-actions Bot commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 671070a4e9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

++ coeff_C_of_ne_zero

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.

No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the t-ring-theory Ring theory label May 20, 2026
eric-wieser
eric-wieser approved these changes May 20, 2026
View reviewed changes

@eric-wieser eric-wieser left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors merge

Thanks!

mathlib-bors Bot pushed a commit that referenced this pull request May 20, 2026
@justus-springer
chore: fix naming of coeff_C_ne_zero (#39632)
ae5f1c0 
Split off from #39623
@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 20, 2026
@mathlib-bors

mathlib-bors Bot commented May 20, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore: fix naming of coeff_C_ne_zero [Merged by Bors] - chore: fix naming of coeff_C_ne_zero May 20, 2026
@mathlib-bors mathlib-bors Bot closed this May 20, 2026
RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 22, 2026
@justus-springer
chore: fix naming of coeff_C_ne_zero (leanprover-community#39632)
664bb1c 
Split off from leanprover-community#39623
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@justus-springer @b-mehta
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
@justus-springer @Bergschaf
chore: fix naming of coeff_C_ne_zero (leanprover-community#39632)
545fbb6 
Split off from leanprover-community#39623
mathlib-bors Bot pushed a commit that referenced this pull request Jun 24, 2026
@justus-springer
feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and `coeff_add…
8b55327 
…_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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes
+1 more reviewer
@wwylele wwylele wwylele approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@justus-springer @eric-wieser @wwylele