eq_natCast' — Mathlib

English

If there is a ring hom f: ℕ →+* R, then f equals the canonical Nat.castRingHom R.

Русский

Если существует кольцевой гомоморфизм f: ℕ →+* R, то f равен каноническому Nat.castRingHom R.

LaTeX

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

Lean4

theorem eq_natCast' [AddMonoidHomClass F ℕ A] (f : F) (h1 : f 1 = 1) : ∀ n : ℕ, f n = n
  | 0 => by simp
  | n + 1 => by rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]

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