Commit 2025-12-12 18:47 a6e07ebf

View on Github →

chore(Algebra/MonoidAlgebra): reduce dependence on defeq abuse, golf (#32604) This is crucial for #25273.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

modified theorem AddMonoidAlgebra.algHom_ext_iff

modified theorem MonoidAlgebra.domCongr_refl

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

modified def AddMonoidAlgebra.of

modified def MonoidAlgebra.singleOneRingHom

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Algebra/MonoidAlgebra/Ideal.lean

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

deleted theorem AddMonoidAlgebra.mem_span_support'

modified theorem AddMonoidAlgebra.mem_span_support

Modified Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean

modified theorem AddMonoidAlgebra.toDirectSum_single

Modified Mathlib/Algebra/Polynomial/Basic.lean

modified theorem Polynomial.ofFinsupp_single

modified theorem Polynomial.toFinsupp_C_mul_X

modified theorem Polynomial.toFinsupp_C_mul_X_pow

modified theorem Polynomial.toFinsupp_X

modified theorem Polynomial.toFinsupp_X_pow

modified theorem Polynomial.toFinsupp_monomial

Modified Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

modified theorem LaurentPolynomial.single_eq_C

modified theorem LaurentPolynomial.single_eq_C_mul_T

modified theorem LaurentPolynomial.single_zero_one_eq_one

modified theorem LaurentPolynomial.smeval_single