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/RCLike/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
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
theorem Complex.nonpos_iff {z : } :
z 0 z.re 0 z.im = 0
theorem Complex.neg_iff {z : } :
z < 0 z.re < 0 z.im = 0
@[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 = abs z 0 z
@[simp]
theorem Complex.neg_re_eq_abs {z : } :
-z.re = abs z z 0
@[simp]
theorem Complex.re_eq_neg_abs {z : } :
z.re = -abs z z 0

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