Commit 2022-04-21 06:55 6012c219
View on Github →refactor(algebra/hom/group): generalize a few lemmas to monoid_hom_class (#13447)
This generalizes a few lemmas to monoid_hom_class from monoid_hom. In particular, monoid_hom.injective_iff has been generalized and renamed to injective_iff_map_eq_one.
This also deletes add_monoid_hom.injective_iff, ring_hom.injective_iff and alg_hom.injective_iff. All of these are superseded by the generically applicable injective_iff_map_eq_zero.