mathlib

4a02fd3b - refactor(algebra/order/ring,data/complex): redefine `ordered_comm_ring` and complex order (#9420)

refactor(algebra/order/ring,data/complex): redefine `ordered_comm_ring` and complex order (#9420) * `ordered_comm_ring` no longer extends `ordered_comm_semiring`. We add an instance `ordered_comm_ring.to_ordered_comm_semiring` instead. * redefine complex order in terms of `re` and `im` instead of existence of a nonnegative real number. * simplify `has_star.star` on `complex` to `conj`; * rename `complex.complex_partial_order` etc to `complex.partial_order` etc, make them protected.