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

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
    @[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