Theorem MonoidAlgebra.coe_add

Modification history

2025-08-31 00:30

Mathlib/Algebra/MonoidAlgebra/Defs.lean

chore(Algebra/MonoidAlgebra): use `to_additive` for `AddMonoidAlgebra` (#29036) …

Modified MonoidAlgebra.coe_add View on Github →

2025-07-22 22:48

Mathlib/Algebra/MonoidAlgebra/Defs.lean

feat(MonoidAlgebra): miscellaneous basic lemmas (#27199) …

Added MonoidAlgebra.coe_add View on Github →