of_to_nat' — Mathlib

English

For every n in Num, Num.ofNat'(n : ℕ) = n, i.e., converting a numeral to Nat and back returns the same numeral.

Русский

Для каждого n из Num: Num.ofNat'(n : ℕ) = n, то есть преобразование цифр в натуральное и обратно возвращает тот же числитель.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem of_to_nat' : ∀ n : Num, Num.ofNat' (n : ℕ) = n
  | 0 => ofNat'_zero
  | pos p => p.of_to_nat'

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