instStarOrderedRing — Mathlib

English

The integers can be endowed with a star-ordered ring structure; in particular there is an involution *, which in the standard realization is the identity on ℤ and preserves the order.

Русский

Целые числа можно наделить структурой звёздового упорядоченного кольца; в частности, существует инволюция *, которая в обычной реализации является тождественной на ℤ и сохраняет порядок.

LaTeX

$$$\mathbb{Z}$ admits a StarOrderedRing structure$$

Lean4

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

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