instZeroLEOneClass

Mathlib.Algebra.Order.Ring.Rat

URI: https://scilib.ai/kg/mathlib#Rat.instZeroLEOneClass

English

ℚ satisfies 0 ≤ 1; the order unit is positive.

Русский

Для ℚ выполняется 0 ≤ 1; единица является положительной величиной.

LaTeX

$$ZeroLEOneClass(\\mathbb{Q})$$

Lean4

instance instZeroLEOneClass : ZeroLEOneClass ℚ where zero_le_one := by decide

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

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

Разделы

Аффилиация

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