map_natCast

Mathlib.Data.Nat.Cast.Basic

URI: https://scilib.ai/kg/mathlib#map_natCast

English

For any RingHomClass f from R to S, f(n) equals the nat cast of n for all natural numbers n.

Русский

Для любого кольцевого гомоморфизма f: R → S выполняется f(n) = n в S для всех n ∈ ℕ.

LaTeX

$$$ f(n) = n \; (n \in \mathbb{N}) $ with nat cast interpretation$$

Lean4

@[simp]
theorem map_natCast [FunLike F R S] [RingHomClass F R S] (f : F) : ∀ n : ℕ, f (n : R) = n :=
  map_natCast' f <| map_one f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru