mathlib

6012c219 - refactor(algebra/hom/group): generalize a few lemmas to `monoid_hom_class` (#13447)

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`.