Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monoid_hom.coe_coe

Modification history

2022-09-30 13:10
src/algebra/hom/group.lean
feat(algebra/hom/group): `simp` lemmas for applying generic morphism coercions (#16700) …
Added monoid_hom.coe_coeView on Github →