Theorem AddMonoidAlgebra.single_ne_zero

Modification history

2025-08-31 00:30

Mathlib/Algebra/MonoidAlgebra/Defs.lean

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

Deleted AddMonoidAlgebra.single_ne_zero View on Github →

2025-04-01 08:50

Mathlib/Algebra/MonoidAlgebra/Defs.lean

feat(Algebra/MonoidAlgebra/Defs): add simple lemmas about `single` (#22982) …

Added AddMonoidAlgebra.single_ne_zero View on Github →