instIsStrictOrderedRing

Mathlib.Algebra.Order.Ring.Rat

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

← MathLib Explorer

English

ℚ is a strict ordered ring; if ab > 0 and cd > 0, then (ac)(bd) > 0 etc. in the ring.

Русский

ℚ является строгово упорядоченным кольцом; умножение сохраняет строгий порядок.

LaTeX

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

Lean4

instance instIsStrictOrderedRing : IsStrictOrderedRing ℚ :=
  .of_mul_pos fun _ _ ha hb ↦ (Rat.mul_nonneg ha.le hb.le).lt_of_ne' (mul_ne_zero ha.ne' hb.ne')

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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