instStarOrderedRing — Mathlib

English

The natural numbers carry a canonical star-ordered ring structure, where the star is the identity and the usual order is used.

Русский

У натуральных чисел существует каноническая звёздно-упорядоченная кольцевая структура: операция звезды есть тождественная, порядок — обычный.

LaTeX

$$StarOrderedRing(\mathbb{N})$$

Lean4

instance instStarOrderedRing : StarOrderedRing ℕ where
  le_iff a
    b :=
    by
    have : AddSubmonoid.closure (range fun x : ℕ ↦ x * x) = ⊤ :=
      eq_top_mono (AddSubmonoid.closure_mono <| singleton_subset_iff.2 <| mem_range.2 ⟨1, one_mul _⟩)
        Nat.addSubmonoidClosure_one
    simp [this, le_iff_exists_add]

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