Mathlib Changelog
Changelog
About
Github
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