Theorem MvPowerSeries.coeff_add_single_C

Modification history

2026-06-24 10:56
Mathlib/RingTheory/MvPowerSeries/Basic.lean
feat(Algebra/MvPolynomial/Basic): `coeff_C_of_ne_zero` and `coeff_add_single_C` (#39623) …
Added MvPowerSeries.coeff_add_single_CView on Github →