of_to_nat — Mathlib

English

For every n in Num, the two-way conversion through natural numbers returns the same numeral: ((n : ℕ) : Num) = n.

Русский

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

LaTeX

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

Lean4

@[simp high, norm_cast]
theorem of_to_nat : ∀ n : Num, ((n : ℕ) : Num) = n :=
  of_to_nat'

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