eq_intCast — Mathlib

English

For any F with FunLike ℤ → α and RingHomClass from ℤ, f n = n for all integers n, i.e., the action of an integer from the domain is the canonical integer in the codomain.

Русский

Для любого F с FunLike ℤ → α и RingHomClass ℤ: f(n) = n для всех целых n, то есть отображение целого числа в α совпадает с каноническим внедрением.

LaTeX

$$$\\forall f:\\mathbb{Z}\\to_+\\alpha,\\forall n\\in\\mathbb{Z},\\ f(n)=n$$$

Lean4

@[simp]
theorem eq_intCast [FunLike F ℤ α] [RingHomClass F ℤ α] (f : F) (n : ℤ) : f n = n :=
  eq_intCast' f (map_one _) n

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