eq_intCast' — Mathlib

English

For any AddGroupWithOne α and any FunLike F ℤ → α with AddMonoidHomClass F ℤ α, if f(1) = 1, then f(n) = n for all integers n.

Русский

Для любого AddGroupWithOne α и любого F: ℤ → α, удовлетворяющего AddMonoidHomClass, если f(1) = 1, то f(n) = n для всех n ∈ ℤ.

LaTeX

$$$$ \\forall f: F,\\ f(1)=1 \\Rightarrow \\forall n \\in \\mathbb{Z}, \\ f(n) = n. $$$$

Lean4

theorem eq_intCast' [AddGroupWithOne α] [FunLike F ℤ α] [AddMonoidHomClass F ℤ α] (f : F) (h₁ : f 1 = 1) :
    ∀ n : ℤ, f n = n :=
  DFunLike.ext_iff.1 <| (f : ℤ →+ α).eq_intCastAddHom h₁

Похожие утверждения