Theorem AddMonoidAlgebra.smul_single

Modification history

2025-08-31 00:30

Mathlib/Algebra/MonoidAlgebra/Defs.lean

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

Deleted AddMonoidAlgebra.smul_single View on Github →

2025-01-23 21:56

Mathlib/Algebra/MonoidAlgebra/Defs.lean

fix: add missing `MonoidAlgebra.smul_single` (#20933) …

Added AddMonoidAlgebra.smul_single View on Github →