# Documentation

Mathlib.Data.Complex.Order

# 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/IsROrC/Basic.lean as

• IsROrC.toStrictOrderedCommRing
• IsROrC.toStarOrderedRing
• IsROrC.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.

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
@[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_ofReal_le {r : } {z : } (hz : r z) :
z = z.re