repr_ofNat

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#ONote.repr_ofNat

English

For all n, repr(ofNat n) = n.

Русский

Для всех n выполняется repr(ofNat n) = n.

LaTeX

$$$\operatorname{repr}(\operatorname{ofNat}(n)) = n$$$

Lean4

@[simp]
theorem repr_ofNat (n : ℕ) : repr (ofNat n) = n := by cases n <;> simp

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

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

Разделы

Аффилиация

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