HepLean 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.

source
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.

Equations
Instances For
    source
    theorem Complex.le_def {z w : ℂ} :
    z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im
    source
    theorem Complex.lt_def {z w : ℂ} :
    z < w ↔ z.re < w.re ∧ z.im = w.im
    source
    theorem Complex.nonneg_iff {z : ℂ} :
    0 ≤ z ↔ 0 ≤ z.re ∧ 0 = z.im
    source
    theorem Complex.pos_iff {z : ℂ} :
    0 < z ↔ 0 < z.re ∧ 0 = z.im
    source
    theorem Complex.nonpos_iff {z : ℂ} :
    z ≤ 0 ↔ z.re ≤ 0 ∧ z.im = 0
    source
    theorem Complex.neg_iff {z : ℂ} :
    z < 0 ↔ z.re < 0 ∧ z.im = 0
    source
    @[simp]
    theorem Complex.real_le_real {x y : ℝ} :
    ↑x ≤ ↑y ↔ x ≤ y
    source
    @[simp]
    theorem Complex.real_lt_real {x y : ℝ} :
    ↑x < ↑y ↔ x < y
    source
    @[simp]
    theorem Complex.zero_le_real {x : ℝ} :
    0 ≤ ↑x ↔ 0 ≤ x
    source
    @[simp]
    theorem Complex.zero_lt_real {x : ℝ} :
    0 < ↑x ↔ 0 < x
    source
    theorem Complex.not_le_iff {z w : ℂ} :
    ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
    source
    theorem Complex.not_lt_iff {z w : ℂ} :
    ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
    source
    theorem Complex.not_le_zero_iff {z : ℂ} :
    ¬z ≤ 0 ↔ 0 < z.re ∨ z.im ≠ 0
    source
    theorem Complex.not_lt_zero_iff {z : ℂ} :
    ¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0
    source
    theorem Complex.eq_re_of_ofReal_le {r : ℝ} {z : ℂ} (hz : ↑r ≤ z) :
    z = ↑z.re
    source
    @[simp]
    theorem Complex.re_eq_abs {z : ℂ} :
    z.re = Complex.abs z ↔ 0 ≤ z
    source
    @[simp]
    theorem Complex.neg_re_eq_abs {z : ℂ} :
    -z.re = Complex.abs z ↔ z ≤ 0
    source
    @[simp]
    theorem Complex.re_eq_neg_abs {z : ℂ} :
    z.re = -Complex.abs z ↔ z ≤ 0
    source
    theorem Complex.monotone_ofReal :
    Monotone Complex.ofReal
    source
    def Mathlib.Meta.Positivity.evalComplexOfReal :
    Mathlib.Meta.Positivity.PositivityExt

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

    Instances For