Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 16:20 a557f8bd

View on Github →

feat(data/complex): order structure (#4684)

Estimated changes

Modified src/data/complex/basic.lean

added def complex.complex_order

added def complex.complex_ordered_comm_ring

added theorem complex.le_def

added theorem complex.lt_def

added theorem complex.norm_sq_eq_conj_mul_self

modified theorem complex.norm_sq_one

modified theorem complex.norm_sq_zero

added theorem complex.real_le_real

added theorem complex.real_lt_real

added theorem complex.zero_le_real

added theorem complex.zero_lt_real