eq_natCast

Mathlib.Data.Nat.Cast.Basic

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

English

For any ring hom f: ℕ →+* R, f equals the canonical Nat.castRingHom.

Русский

Для кольцевого гомоморфизма f: ℕ →+* R выполняется f = Nat.castRingHom R.

LaTeX

$$$ f = \operatorname{Nat}.castRingHom(R) $$$

Lean4

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

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

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

Разделы

Аффилиация

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