Commit 2022-09-30 13:10 cc967daa
View on Github →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.