English
If two MonoidHom f,g: ℤ →* M agree on -1 and on all natural numbers, then f = g.
Русский
Если два MonoidHom f,g: ℤ →* M совпадают на -1 и на всех натуральных, то f = g.
LaTeX
$$$$ \\forall f,g : \\mathbb{Z} \\to^* M,\\ f(-1) = g(-1) \\land f \\circ \\mathrm{Int.ofNatHom} = g \\circ \\mathrm{Int.ofNatHom} \\Rightarrow f = g. $$$$
Lean4
/-- If two `MonoidHom`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.toMonoidHom = g.comp Int.ofNatHom.toMonoidHom) : f = g :=
by
ext (x | x)
· exact (DFunLike.congr_fun h_nat x :)
· rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
congr 1
exact mod_cast (DFunLike.congr_fun h_nat (x + 1) :)
