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 in Mathlib/Analysis/RCLike/Basic.lean as

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

These are all only available with open scoped ComplexOrder.

def Complex.partialOrder : PartialOrder ℂ

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.

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

theorem Complex.sq_nonneg_iff {z : ℂ} : 0 ≤ z ^ 2 ↔ z.im = 0

theorem Complex.sq_nonpos_iff {z : ℂ} : z ^ 2 ≤ 0 ↔ z.re = 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_norm {z : ℂ} : z.re = ‖z‖ ↔ 0 ≤ z

@[simp]

theorem Complex.neg_re_eq_norm {z : ℂ} : -z.re = ‖z‖ ↔ z ≤ 0

@[simp]

theorem Complex.re_eq_neg_norm {z : ℂ} : z.re = -‖z‖ ↔ z ≤ 0

theorem Complex.monotone_ofReal : Monotone ofReal

theorem Mathlib.Meta.Positivity.ofReal_pos {x : ℝ} : 0 < x → 0 < ↑x

Alias of the reverse direction of Complex.zero_lt_real.

theorem Mathlib.Meta.Positivity.ofReal_nonneg {x : ℝ} : 0 ≤ x → 0 ≤ ↑x

Alias of the reverse direction of Complex.zero_le_real.

theorem Mathlib.Meta.Positivity.ofReal_ne_zero_of_ne_zero {z : ℝ} : z ≠ 0 → ↑z ≠ 0

Alias of the reverse direction of Complex.ofReal_ne_zero.

def Mathlib.Meta.Positivity.evalComplexOfReal : PositivityExt

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