Commit 2026-06-24 10:56 8b553276

View on Github →

feat(Algebra/MvPolynomial/Basic): coeff_C_of_ne_zero and coeff_add_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.

depends on: #39632

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.coeff_C_of_ne_zero

added theorem MvPolynomial.coeff_add_single_C

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

added theorem MvPowerSeries.coeff_C_of_ne_zero

added theorem MvPowerSeries.coeff_add_single_C