Theorem OneHom.coe_id

Modification history

2025-01-29 00:09
Mathlib/Algebra/Group/Hom/Defs.lean
feat(Algebra): add `MonoidHom.coe_id` (#21189) …
Added OneHom.coe_idView on Github →