Commit 2021-09-28 11:33 4a02fd3b

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.