Theorem AddMonoid.End.coe_one

Modification history

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 →