English
In the setting above, 0 ≤ x if and only if there exists s ∈ R with x = star(s) · s.
Русский
В данной обстановке 0 ≤ x тогда и только тогда, когда существует s ∈ R такое, что x = star(s) · s.
LaTeX
$$$0 \le x \iff \exists s:\; R,\ x = \star s \cdot s$$$
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 of the form `star s * s`
for `s : R`.
This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or
any C⋆-algebra), and obviates the hassle of `AddSubmonoid.closure_induction` when creating those
instances. -/
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 ↔ ∃ s, x = star s * s) : StarOrderedRing R :=
of_le_iff <| by
have : AddLeftMono R := ⟨fun _ _ _ h => h_add h _⟩
simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)
