toZeroLeOneClass

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#CanonicallyOrderedAdd.toZeroLeOneClass

English

For canonically ordered additive monoids, 0 ≤ 1 holds as part of the ZeroLeOneClass.

Русский

Для канонически упорядоченных аддитивных монойдов верно 0 ≤ 1 как часть класса ZeroLeOne.

LaTeX

$$$0 \le 1$$$

Lean4

instance (priority := 100) toZeroLeOneClass [AddZeroClass α] [LE α] [CanonicallyOrderedAdd α] [One α] :
    ZeroLEOneClass α :=
  ⟨zero_le 1⟩

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

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

Разделы

Аффилиация

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