map_intCast' — Mathlib

English

If F is AddGroupWithOne-valued and f : F respects integers into α, then f(n) = n for all n when f(1) = 1.

Русский

Если F удовлетворяет группу с единицей и f применимо к целым значениям в α, то f(n) = n при f(1) = 1.

LaTeX

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

Lean4

/-- This version is primed so that the `RingHomClass` versions aren't. -/
theorem map_intCast' [AddGroupWithOne α] [AddGroupWithOne β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F)
    (h₁ : f 1 = 1) : ∀ n : ℤ, f n = n :=
  eq_intCast' ((f : α →+ β).comp <| Int.castAddHom _) (by simpa)

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