feat(data/int/cast): monoid_hom.ext_int (#3587)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/data/int/cast.lean

@@ -184,6 +184,20 @@ ext_iff.1 (f.eq_int_cast_hom h1)
 
 end add_monoid_hom
 
+namespace monoid_hom
+variables {M : Type*} [monoid M]
+open multiplicative
+
+theorem ext_int {f g : multiplicative ℤ →* M}
+  (h1 : f (of_add 1) = g (of_add 1)) : f = g :=
+begin
+  ext,
+  exact add_monoid_hom.ext_iff.1
+    (@add_monoid_hom.ext_int _ _ f.to_additive g.to_additive h1) _,
+end
+
+end monoid_hom
+
 namespace ring_hom
 
 variables {α : Type*} {β : Type*} [ring α] [ring β]