# Commit 2021-09-28 11:33 4a02fd3b

View on Github →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.