English
On a RCLike type K there exists a strict order making it a strictly ordered ring, namely z ≤ w if and only if w − z is real and nonnegative.
Русский
На типе K существует строгий порядок, делающий его строго упорядоченным кольцом: $z \le w$ тогда и только тогда, когда $w - z$ является вещественным неотрицательным числом.
LaTeX
$$$z \le w \iff (w - z) \in \mathbb{R} \ \land\ 0 \le (w - z)$$$
Lean4
/-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℝ` and `ℂ` are strictly ordered rings.
Note this is only an instance with `open scoped ComplexOrder`. -/
theorem toIsStrictOrderedRing : IsStrictOrderedRing K :=
.of_mul_pos fun z w hz hw ↦ by
rw [lt_iff_re_im, map_zero] at hz hw ⊢
simp [mul_re, mul_im, ← hz.2, ← hw.2, mul_pos hz.1 hw.1]
