to_of_nat — Mathlib

English

For every natural number n, casting to Num and back yields the original n: ((n : Num) : ℕ) = n.

Русский

Для любого натурального числа n повторное приведение к Num и обратно даёт исходное n: ((n : Num) : ℕ) = n.

LaTeX

$$$\\forall n : \\mathbb{N}, ((n : Num) : \\mathbb{N}) = n$$$

Lean4

theorem to_of_nat : ∀ n : ℕ, ((n : Num) : ℕ) = n
  | 0 => by rw [Nat.cast_zero, cast_zero]
  | n + 1 => by rw [Nat.cast_succ, add_one, succ_to_nat, to_of_nat n]

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