Theorem MvPolynomial.coeff_add_single_C

Modification history

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