feat(algebra/group/hom): `monoid_with_zero_hom.to_monoid_hom_injectiv…

…e` and co. (#7174)

This came up in #6788.

src/algebra/group/hom.lean

@@ -511,6 +511,21 @@ lemma monoid_with_zero_hom.cancel_left
         ← monoid_with_zero_hom.comp_apply, h, monoid_with_zero_hom.comp_apply],
  λ h, h ▸ rfl⟩
 
+@[to_additive]
+lemma monoid_hom.to_one_hom_injective [mul_one_class M] [mul_one_class N] :
+  function.injective (monoid_hom.to_one_hom : (M →* N) → one_hom M N) :=
+λ f g h, monoid_hom.ext $ one_hom.ext_iff.mp h
+@[to_additive]
+lemma monoid_hom.to_mul_hom_injective [mul_one_class M] [mul_one_class N] :
+  function.injective (monoid_hom.to_mul_hom : (M →* N) → mul_hom M N) :=
+λ f g h, monoid_hom.ext $ mul_hom.ext_iff.mp h
+lemma monoid_with_zero_hom.to_monoid_hom_injective [monoid_with_zero M] [monoid_with_zero N] :
+  function.injective (monoid_with_zero_hom.to_monoid_hom : monoid_with_zero_hom M N → M →* N) :=
+λ f g h, monoid_with_zero_hom.ext $ monoid_hom.ext_iff.mp h
+lemma monoid_with_zero_hom.to_zero_hom_injective [monoid_with_zero M] [monoid_with_zero N] :
+  function.injective (monoid_with_zero_hom.to_zero_hom : monoid_with_zero_hom M N → zero_hom M N) :=
+λ f g h, monoid_with_zero_hom.ext $ zero_hom.ext_iff.mp h
+
 @[simp, to_additive] lemma one_hom.comp_id [has_one M] [has_one N]
   (f : one_hom M N) : f.comp (one_hom.id M) = f := one_hom.ext $ λ x, rfl
 @[simp, to_additive] lemma mul_hom.comp_id [has_mul M] [has_mul N]