Commutative star-ordered rings are ordered rings #
A noncommutative star-ordered ring is generally not an ordered ring. Indeed, in a star-ordered ring, nonnegative elements are self-adjoint, but the product of self-adjoint elements is self-adjoint if and only if they commute. Therefore, a necessary condition for a star-ordered ring to be an ordered ring is that all nonnegative elements commute. Consequently, if a star-ordered ring is spanned by it nonnegative elements (as is the case for C⋆-algebras) and it is also an ordered ring, then it is commutative.
In this file we prove the converse: a commutative star-ordered ring is an ordered ring.
instance
StarOrderedRing.toIsOrderedRing
(R : Type u_1)
[CommSemiring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
:
A commutative star-ordered semiring is an ordered semiring.