instMulArchimedean — Mathlib

English

The set of nonnegative elements of a MulArchimedean ordered ring is MulArchimedean.

Русский

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

LaTeX

$$$$ \text{MulArchimedean}\left(\{ x \in R \mid 0 \le x \} \right). $$$$

Lean4

instance instMulArchimedean [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R]
    [ExistsAddOfLE R] : MulArchimedean { x : R // 0 ≤ x } :=
  ⟨fun x _ hy ↦ (pow_unbounded_of_one_lt x hy).imp fun _ h ↦ h.le⟩

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