# The partial order on the complex numbers #

This order is defined by z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im.

This is a natural order on ℂ because, as is well-known, there does not exist an order on ℂ making it into a LinearOrderedField. However, the order described above is the canonical order stemming from the structure of ℂ as a ⋆-ring (i.e., it becomes a StarOrderedRing). Moreover, with this order ℂ is a StrictOrderedCommRing and the coercion (↑) : ℝ → ℂ is an order embedding.

This file only provides Complex.partialOrder and lemmas about it. Further structural classes are provided by Mathlib/Data/RCLike/Basic.lean as

• RCLike.toStrictOrderedCommRing
• RCLike.toStarOrderedRing
• RCLike.toOrderedSMul

These are all only available with open scoped ComplexOrder.

We put a partial order on ℂ so that z ≤ w exactly if w - z is real and nonnegative. Complex numbers with different imaginary parts are incomparable.

Equations
Instances For
theorem Complex.le_def {z : } {w : } :
z w z.re w.re z.im = w.im
theorem Complex.lt_def {z : } {w : } :
z < w z.re < w.re z.im = w.im
theorem Complex.nonneg_iff {z : } :
0 z 0 z.re 0 = z.im
theorem Complex.pos_iff {z : } :
0 < z 0 < z.re 0 = z.im
@[simp]
theorem Complex.real_le_real {x : } {y : } :
x y x y
@[simp]
theorem Complex.real_lt_real {x : } {y : } :
x < y x < y
@[simp]
theorem Complex.zero_le_real {x : } :
0 x 0 x
@[simp]
theorem Complex.zero_lt_real {x : } :
0 < x 0 < x
theorem Complex.not_le_iff {z : } {w : } :
¬z w w.re < z.re z.im w.im
theorem Complex.not_lt_iff {z : } {w : } :
¬z < w w.re z.re z.im w.im
theorem Complex.not_le_zero_iff {z : } :
¬z 0 0 < z.re z.im 0
theorem Complex.not_lt_zero_iff {z : } :
¬z < 0 0 z.re z.im 0
theorem Complex.eq_re_of_ofReal_le {r : } {z : } (hz : r z) :
z = z.re
@[simp]
theorem Complex.re_eq_abs {z : } :
z.re = Complex.abs z 0 z
@[simp]
theorem Complex.neg_re_eq_abs {z : } :
-z.re = Complex.abs z z 0
@[simp]
theorem Complex.re_eq_neg_abs {z : } :
z.re = -Complex.abs z z 0

Extension for the positivity tactic: Complex.ofReal is positive/nonnegative/nonzero if its input is.

Instances For