instStarOrderedRing — Mathlib

English

Let the rational numbers ℚ carry their standard order and the usual involution. Then (ℚ, +, *, 0, 1, *) with this involution forms a star-ordered ring.

Русский

Пусть для рациональных чисел ℚ задан обычный порядок и обычная унарная инволюция. Тогда (ℚ, +, ·, 0, 1) с этой инволюцией образуют звёздочно-упорядоченное кольцо.

LaTeX

$$$\mathrm{StarOrderedRing}(\mathbb{Q})$$$

Lean4

instance instStarOrderedRing : StarOrderedRing ℚ where
  le_iff a b := by simp [eq_comm, le_iff_exists_nonneg_add (a := a)]

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