map_intCast — Mathlib

English

For any F with FunLike α → β and RingHomClass F α β, f n = n for all integers n; the map respects integer cast.

Русский

Для любого F с FunLike α → β и RingHomClass F α β, f n = n для всех целых n; отображение сохраняет целочисленную инъекцию.

LaTeX

$$$\\forall f:\\,F,\\forall n:\\mathbb{Z},\\ f n = n$$$

Lean4

@[simp]
theorem map_intCast [FunLike F α β] [RingHomClass F α β] (f : F) (n : ℤ) : f n = n :=
  eq_intCast ((f : α →+* β).comp (Int.castRingHom α)) n

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