Commit 2024-04-05 15:59 bfa88435

feat: make StarOrderedRing a mixin (#11872) This makes StarOrderedRing take StarRing as a parameter instead of extending it, and as a result moves the typeclass to Prop. It was already a mixin with respect to the order and algebraic structure. There are two primary motivations:

1. This makes it possible to directly assume that C(α, R) is a StarOrderedRing with [StarOrderedRing C(α, R)], as currently there is no typeclass on R which would naturally guarantee this property. This is relevant as we want this type class on continuous functions for the continuous functional calculus.
2. We will eventually want a StarOrderedRing instance on C(α, A) where A is a complex (or even real) C⋆-algebra, and making this a mixin avoids loops with StarRing.