instNeZeroOne

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.instNeZeroOne

English

In NatOrdinal, the element 1 is not zero.

Русский

В NatOrdinal элемент 1 не равен нулю.

LaTeX

$$$1 \\neq 0$$$

Lean4

instance instNeZeroOne : NeZero (1 : NatOrdinal) :=
  Ordinal.instNeZeroOne

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

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

Разделы

Аффилиация

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