Commit 2026-11-02 08:15 dd67281f

View on Github →

refactor(Algebra/Polynomial): make into an abbrev of AddMonoidAlgebra (#41981) ... and deprecate the declarations that are now tautological (toFinsupp/ofFinsupp, coeff and their API). For some of the Polynomial declarations that needed changing, it was simplest to replace them with the corresponding AddMonoidAlgebra one. Note that this replacement is far from exhaustive (a majority of the Polynomial API could be replaced this way). Note that algebraMap R R[X] has changed defeq. Zulip Generated through several rounds of manual review with Claude Opus. Heavily edited by hand afterwards. Assisted-by: Claude Opus 4.8

Estimated changes

added theorem Polynomial.X_eq_single
deleted def Polynomial.coeff
modified theorem Polynomial.coeff_C_zero
modified theorem Polynomial.coeff_X
modified theorem Polynomial.coeff_X_one
modified theorem Polynomial.coeff_X_zero
deleted theorem Polynomial.coeff_inj
modified theorem Polynomial.coeff_monomial
modified theorem Polynomial.coeff_neg
modified theorem Polynomial.coeff_ofFinsupp
modified theorem Polynomial.coeff_ofNat_succ
modified theorem Polynomial.coeff_ofNat_zero
deleted theorem Polynomial.coeff_one_zero
modified theorem Polynomial.coeff_sub
deleted def Polynomial.erase
modified theorem Polynomial.erase_monomial
modified theorem Polynomial.erase_same
deleted theorem Polynomial.erase_zero
modified theorem Polynomial.eta
deleted theorem Polynomial.ext
deleted theorem Polynomial.ext_iff
modified theorem Polynomial.ofFinsupp_add
modified theorem Polynomial.ofFinsupp_eq_one
modified theorem Polynomial.ofFinsupp_inj
modified theorem Polynomial.ofFinsupp_mul
modified theorem Polynomial.ofFinsupp_neg
modified theorem Polynomial.ofFinsupp_nsmul
modified theorem Polynomial.ofFinsupp_ofNat
modified theorem Polynomial.ofFinsupp_one
modified theorem Polynomial.ofFinsupp_pow
modified theorem Polynomial.ofFinsupp_single
modified theorem Polynomial.ofFinsupp_sub
modified theorem Polynomial.ofFinsupp_zero
modified theorem Polynomial.sum_monomial_eq
modified def Polynomial.support
modified theorem Polynomial.toFinsupp_C
modified theorem Polynomial.toFinsupp_X_pow
modified theorem Polynomial.toFinsupp_apply
modified theorem Polynomial.toFinsupp_eq_one
modified theorem Polynomial.toFinsupp_erase
modified theorem Polynomial.toFinsupp_inj
modified theorem Polynomial.toFinsupp_pow
modified theorem Polynomial.toFinsupp_zero
deleted def Polynomial.update
deleted structure Polynomial
modified theorem Polynomial.coeff_C_mul
modified theorem Polynomial.coeff_add
modified theorem Polynomial.coeff_mul_C
deleted theorem Polynomial.coeff_smul
modified theorem Polynomial.smul_eq_C_mul
modified theorem Polynomial.eraseLead_zero
modified theorem Polynomial.map_id
modified theorem Polynomial.map_injective
modified theorem Polynomial.map_map
modified theorem Polynomial.contract_one
modified theorem Polynomial.expand_injective
modified theorem Polynomial.X_mul_divX_add
modified theorem Polynomial.divX_C
modified theorem Polynomial.divX_add
modified theorem Polynomial.divX_mul_X_add
modified theorem Polynomial.mirror_mirror
modified theorem Polynomial.mirror_natDegree
modified theorem minpoly.coeff_zero_eq_zero
modified theorem minpoly.coeff_zero_ne_zero
modified theorem coeff_minpolyDiv
modified theorem Derivation.mapCoeffs_apply
modified theorem Polynomial.restriction_one
modified theorem exists_C_coeff_notMem
modified theorem mem_span_C_coeff
modified theorem Polynomial.coe_def
modified theorem Polynomial.coeff_coe
modified theorem PowerSeries.trunc_C
modified theorem PowerSeries.trunc_one