mathlib

cc967daa - feat(algebra/hom/group): `simp` lemmas for applying generic morphism coercions (#16700)

feat(algebra/hom/group): `simp` lemmas for applying generic morphism coercions (#16700) There are a bunch of random specific versions of these lemmas floating around, which can be made generic to apply to all `one_hom_class`/`mul_hom_class`/`monoid_hom_class` instances. Compare existing `ring_hom.coe_coe`.