Commit 2025-12-08 07:46 75d63000

View on Github →

feat(Algebra/MonoidAlgebra): extend the R[M] notation to MonoidAlgebra R M (#30877) It currently only is notation for AddMonoidAlgebra R M.

Estimated changes

modified theorem AddMonoidAlgebra.lift_apply
modified theorem MonoidAlgebra.algHom_ext'
modified theorem MonoidAlgebra.algHom_ext
modified def MonoidAlgebra.lift
modified theorem MonoidAlgebra.lift_apply'
modified theorem MonoidAlgebra.lift_apply
modified theorem MonoidAlgebra.lift_unique'
modified theorem MonoidAlgebra.lift_unique
modified theorem MonoidAlgebra.addHom_ext'
modified theorem MonoidAlgebra.coe_add
modified theorem MonoidAlgebra.ext
modified theorem MonoidAlgebra.induction_on
modified theorem MonoidAlgebra.intCast_def
modified def MonoidAlgebra.mul'
modified theorem MonoidAlgebra.mul_apply
modified theorem MonoidAlgebra.mul_def
modified theorem MonoidAlgebra.natCast_def
modified theorem MonoidAlgebra.neg_apply
modified def MonoidAlgebra.of
modified def MonoidAlgebra.ofMagma
modified theorem MonoidAlgebra.of_commute
modified theorem MonoidAlgebra.one_def
modified theorem MonoidAlgebra.ringHom_ext'
modified theorem MonoidAlgebra.ringHom_ext
modified theorem MonoidAlgebra.single_zero
modified theorem MonoidAlgebra.smul_apply
modified theorem MonoidAlgebra.sum_single
modified def MonoidAlgebra.liftNC
modified theorem MonoidAlgebra.mapDomain_sum
modified theorem MonoidAlgebra.support_mul
modified theorem MonoidAlgebra.support_one
modified def Rep.counitIso
modified def Rep.counitIsoAddEquiv
added theorem test_1
added theorem test_2