Theorem MonoidHom.coe_id

Modification history

2025-09-29 08:46
Mathlib/Algebra/Group/Hom/Defs.lean
feat(Algebra/Group/Hom/Defs): MonoidHom switching from MulOneClass to MulOne (#28702) …
Modified MonoidHom.coe_idView on Github →
2025-01-29 00:09
Mathlib/Algebra/Group/Hom/Defs.lean
feat(Algebra): add `MonoidHom.coe_id` (#21189) …
Added MonoidHom.coe_idView on Github →