Theorem Monoid.End.coe_one

Modification history

2025-01-20 16:09
Mathlib/Algebra/Group/Hom/Defs.lean
feat: use to_additive for Monoid.End (#19687) …
Added Monoid.End.coe_oneView on Github →