instIsStrictOrderedRingNNRat

Mathlib.Data.NNRat.Order

URI: https://scilib.ai/kg/mathlib#instIsStrictOrderedRingNNRat

English

The nonnegative rationals ℚ≥0 form a strict ordered ring.

Русский

Неотрицательные рациональные числа ℚ≥0 образуют строго упорядоченное кольцо.

LaTeX

$$$\\mathbb{Q}_{\\ge 0} \\\\text{ is a strict ordered ring.}$$$

Lean4

instance : IsStrictOrderedRing ℚ≥0 :=
  Nonneg.isStrictOrderedRing

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

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

Разделы

Аффилиация

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