English
In a star-ordered ring with a nonunital ring structure, provided the order is compatible with addition, a nonnegative element x is exactly the elements of the additive submonoid closure of star(s) · s as s runs over R.
Русский
В звездоупорядоченном кольце с ненулевой структурой кольца, если порядок совместим с сложением, неотрицательный элемент x есть ровно элементы замкнутого по сложению подмоноида множества star(s) · s, где s пробегает R.
LaTeX
$$$0 \le x \iff x \in \operatorname{AddSubmonoid.closure}\big(\operatorname{Set.range}(\lambda s:R, \star s \cdot s)\big)$$$
Lean4
/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
show that the nonnegative elements are precisely those elements in the `AddSubmonoid` generated
by `star s * s` for `s : R`. -/
theorem of_nonneg_iff [NonUnitalRing R] [PartialOrder R] [StarRing R] (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
(h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s)) : StarOrderedRing R
where
le_iff x
y := by
have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x)
