nat

Mathlib.SetTheory.Ordinal.Notation

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

English

There is a canonical OfNat ONote instance for natural numbers defined by ofNat.

Русский

Существует каноническое кольцо OfNat ONote для натуральных чисел, заданное через ofNat.

LaTeX

$$$\text{OfNat}(ONote)\;\text{structure for }\mathbb{N}\\$$

Lean4

instance (priority := low) nat (n : ℕ) : OfNat ONote n where ofNat := ofNat n

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

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

Разделы

Аффилиация

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