Structure AddMonoidAlgebra

Modification history

2026-07-04 08:56

Mathlib/Algebra/MonoidAlgebra/Defs.lean

refactor(Algebra): make `MonoidAlgebra` into a one-field structure (#38714) …

Added AddMonoidAlgebra View on Github →

2026-02-15 11:14

MathlibTest/toAdditive.lean

feat(to_additive): automatically infer `relevant_arg` (#35318) …

Added AddMonoidAlgebra View on Github →