English
Two MonoidWithZeroHom f,g: ℤ →*₀ M are equal if they coincide on -1 and on the naturals (via ext).
Русский
Два MonoidWithZeroHom f,g: ℤ →*₀ M равны, если они совпадают на -1 и на натуралах (через эквивалентность).
LaTeX
$$$$ \\forall f,g : \\mathbb{Z} \\to^{*0} M,\\ f(-1) = g(-1) \\land f \\circ \\mathrm{Int.ofNatHom} = g \\circ \\mathrm{Int.ofNatHom} \\Rightarrow f = g. $$$$
Lean4
/-- If two `MonoidWithZeroHom`s agree on `-1` and the naturals then they are equal. -/
@[ext]
theorem ext_int {f g : ℤ →*₀ M} (h_neg_one : f (-1) = g (-1))
(h_nat : f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom) : f = g :=
toMonoidHom_injective <| MonoidHom.ext_int h_neg_one <| MonoidHom.ext (DFunLike.congr_fun h_nat :)
