English
If two MonoidWithZero α-homomorphisms f,g: ℤ →*₀ α agree on -1 and on all positive naturals, then f = g.
Русский
Если два гомоморфизма MonoidWithZero α из ℤ в α согласуются на -1 и на положительных натуральных, то они равны.
LaTeX
$$$$ [MonoidWithZero α] [FunLike F \\mathbb{Z} \\alpha] [MonoidWithZeroHomClass F \\mathbb{Z} \\alpha] \\Rightarrow \\text{ext_int' } f g. $$$$
Lean4
/-- If two `MonoidWithZeroHom`s agree on `-1` and the _positive_ naturals then they are equal. -/
theorem ext_int' [MonoidWithZero α] [FunLike F ℤ α] [MonoidWithZeroHomClass F ℤ α] {f g : F}
(h_neg_one : f (-1) = g (-1)) (h_pos : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
(DFunLike.ext _ _) fun n =>
haveI :=
DFunLike.congr_fun
(@MonoidWithZeroHom.ext_int _ _ (f : ℤ →*₀ α) (g : ℤ →*₀ α) h_neg_one <| MonoidWithZeroHom.ext_nat (h_pos _)) n
this
