Theorem Monoid.coe_one

Modification history

2025-01-20 16:09

Mathlib/Algebra/Group/Hom/Defs.lean

feat: use to_additive for Monoid.End (#19687) …

Deleted Monoid.coe_one View on Github →

2022-12-02 23:34

Mathlib/Algebra/Hom/Group.lean

feat: port Algebra.Hom.Group (#659) …

Added Monoid.coe_one View on Github →