Commit 2023-08-09 17:44 65acf0f1

View on Github →

chore(Data/Complex): move order to a separate file (#6457) Given how confusing this order could be to newcomers, it's probably not reasonable to call it Basic. At any rate, Data/Complex/Basic is very long, and this is an easy split.

Estimated changes

deleted theorem Complex.eq_re_ofReal_le
deleted theorem Complex.le_def
deleted theorem Complex.lt_def
deleted theorem Complex.not_le_iff
deleted theorem Complex.not_le_zero_iff
deleted theorem Complex.not_lt_iff
deleted theorem Complex.not_lt_zero_iff
deleted theorem Complex.real_le_real
deleted theorem Complex.real_lt_real
deleted theorem Complex.zero_le_real
deleted theorem Complex.zero_lt_real
added theorem Complex.le_def
added theorem Complex.lt_def
added theorem Complex.not_le_iff
added theorem Complex.not_lt_iff
added theorem Complex.real_le_real
added theorem Complex.real_lt_real
added theorem Complex.zero_le_real
added theorem Complex.zero_lt_real