Commit 2026-09-02 14:25 631b214f

View on Github →

refactor(Algebra/MvPolynomial): delete coeff (#41427) ... without a deprecation because we want dot notation to resolve to AddMonoidAlgebra.coeff. For migration, replace bare MvPolynomial.coeffs with AddMonoidAlgebra.coeff. Dot notation .coeff will resolve to AddMonoidAlgebra.coeff without further change. MvPolynomial.coeff m p corresponds to AddMonoidAlgebra.coeff p m, so you will need to swap arguments. Note further that AddMonoidAlgebra.coeff p is bundled as a Finsupp while MvPolynomial.coeff is a bare function.

Estimated changes

modified theorem MvPolynomial.as_sum
deleted def MvPolynomial.coeff
modified theorem MvPolynomial.coeff_C_mul
deleted theorem MvPolynomial.coeff_add
modified theorem MvPolynomial.coeff_one
deleted theorem MvPolynomial.coeff_zero
modified theorem MvPolynomial.coeff_zero_C
modified theorem MvPolynomial.coeff_zero_X
modified theorem MvPolynomial.coeff_zero_one
modified theorem MvPolynomial.eq_zero_iff
modified theorem MvPolynomial.ext
modified theorem MvPolynomial.ne_zero_iff
modified theorem MvPolynomial.coeff_neg
modified theorem MvPolynomial.coeff_sub
modified theorem MvPolynomial.coeff_map
modified theorem MvPolynomial.coe_def
modified theorem MvPolynomial.coeff_coe