Commit 2026-03-18 11:57 82b3f55a

View on Github →

feat(Algebra/MonoidAlgebra): explicit conversion functions to/from Finsupp (#36762) Introduce coeff : R[M] → M →₀ R and ofCoeff : (M →₀ R) → R[M] as a way to convert explicitly between MonoidAlgebra and Finsupp and thus avoid defeq abuse. These will be used more widely in future PRs.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

added def MonoidAlgebra.coeff

added def MonoidAlgebra.coeffAddEquiv

added def MonoidAlgebra.coeffEquiv

added theorem MonoidAlgebra.coeff_add

added theorem MonoidAlgebra.coeff_eq_zero

added theorem MonoidAlgebra.coeff_finsuppSum

added theorem MonoidAlgebra.coeff_inj

added theorem MonoidAlgebra.coeff_injective

added theorem MonoidAlgebra.coeff_neg

added theorem MonoidAlgebra.coeff_ofCoeff

added theorem MonoidAlgebra.coeff_smul

added theorem MonoidAlgebra.coeff_sub

added theorem MonoidAlgebra.coeff_sum

added theorem MonoidAlgebra.coeff_zero

added def MonoidAlgebra.ofCoeff

added theorem MonoidAlgebra.ofCoeff_add

added theorem MonoidAlgebra.ofCoeff_coeff

added theorem MonoidAlgebra.ofCoeff_eq_zero

added theorem MonoidAlgebra.ofCoeff_finsuppSum

added theorem MonoidAlgebra.ofCoeff_inj

added theorem MonoidAlgebra.ofCoeff_injective

added theorem MonoidAlgebra.ofCoeff_neg

added theorem MonoidAlgebra.ofCoeff_smul

added theorem MonoidAlgebra.ofCoeff_sub

added theorem MonoidAlgebra.ofCoeff_sum

added theorem MonoidAlgebra.ofCoeff_zero

added theorem MonoidAlgebra.«exists»

added theorem MonoidAlgebra.«forall»

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean