Theorem AddMonoid.End.coe_one

Modification history

2025-01-20 16:09
Mathlib/Algebra/Group/Hom/Defs.lean
feat: use to_additive for Monoid.End (#19687) …
Deleted AddMonoid.End.coe_oneView on Github →
2024-06-05 08:10
Mathlib/Algebra/Group/Hom/Defs.lean
refactor: Redefine `pow` in terms of `iterate` (#1388) …
Added AddMonoid.End.coe_oneView on Github →