three

Mathlib.Algebra.Order.Monoid.NatCast

URI: https://scilib.ai/kg/mathlib#ZeroLEOneClass.neZero.three

English

The number three is nonzero under the default assumptions.

Русский

Число три ненулевое под предпосылками.

LaTeX

$$NeZero 3$$

Lean4

instance three : NeZero (3 : α) :=
  ⟨zero_lt_three.ne'⟩

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

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

Разделы

Аффилиация

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