Commit 2026-09-02 15:10 a99f19be

View on Github →

chore(Algebra/SkewMonoidAlgebra): deprecate sum (#41403) One should just use Finsupp.sum instead.

Estimated changes

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

added theorem SkewMonoidAlgebra.coeff_finsuppSum

deleted theorem SkewMonoidAlgebra.coeff_mapDomain

modified theorem SkewMonoidAlgebra.coeff_mul

deleted theorem SkewMonoidAlgebra.coeff_sum'

deleted theorem SkewMonoidAlgebra.coeff_sum

modified def SkewMonoidAlgebra.mapDomain

modified theorem SkewMonoidAlgebra.mapDomain_comp

modified theorem SkewMonoidAlgebra.mapDomain_id

modified theorem SkewMonoidAlgebra.mapDomain_single

added theorem SkewMonoidAlgebra.ofCoeff_finsuppSum

deleted theorem SkewMonoidAlgebra.ofCoeff_sum

added theorem SkewMonoidAlgebra.sum_coeff_single

modified theorem SkewMonoidAlgebra.sum_single

Modified Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Support.lean

modified theorem SkewMonoidAlgebra.support_sum

Modified Mathlib/Algebra/SkewPolynomial/Basic.lean

modified theorem SkewPolynomial.sum_C_index