Commit 2025-08-31 00:30 b81a8b66

View on Github →

chore(Algebra/MonoidAlgebra): use to_additive for AddMonoidAlgebra (#29036) This PR uses to_additive to define AddMonoidAlgebra, instead of copying all of the definitions and theorems by hand.

Estimated changes

modified theorem MonoidAlgebra.domCongr_refl
modified theorem MonoidAlgebra.domCongr_symm
deleted theorem AddMonoidAlgebra.coe_add
deleted theorem AddMonoidAlgebra.ext
deleted theorem AddMonoidAlgebra.mul_def
deleted theorem AddMonoidAlgebra.one_def
deleted def AddMonoidAlgebra
modified theorem MonoidAlgebra.coe_add
modified theorem MonoidAlgebra.neg_apply