English
A star-ordered ring structure exists on K, characterized by z ≤ w if and only if w − z is real and nonnegative, with nonnegatives being exactly the elements of the form t* t.
Русский
На K существует звездоупорядоченное кольцо: z ≤ w тогда и только тогда, когда w − z вещественно и неотрицательно, а неотрицательные элементы есть именно в виде t* t.
LaTeX
$$$ \text{StarOrderedRing}(K) \text{ with } z \le w \iff w - z \text{ is real and nonnegative; } \{t^* t : t \in K\} \text{ are the nonnegatives} $$$
Lean4
/-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℝ` and `ℂ` are star ordered rings.
(That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)
Note this is only an instance with `open scoped ComplexOrder`. -/
theorem toStarOrderedRing : StarOrderedRing K :=
StarOrderedRing.of_nonneg_iff' (h_add := fun {x y} hxy z =>
by
rw [RCLike.le_iff_re_im] at *
simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy) (h_nonneg_iff := fun x =>
by
rw [nonneg_iff]
refine ⟨fun h ↦ ⟨√(re x), by simp [ext_iff (K := K), h.1, h.2]⟩, ?_⟩
rintro ⟨s, rfl⟩
simp [mul_comm, mul_self_nonneg, add_nonneg])
