# 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.

A commutative star-ordered semiring is an ordered semiring.

This is not registered as an instance because it introduces a type class loop between `CommSemiring`

and `OrderedCommSemiring`

, and it seem loops still cause issues sometimes.

See note [reducible non-instances].

## Equations

- StarOrderedRing.toOrderedCommSemiring R = OrderedCommSemiring.mk (_ : ā (a b : R), a * b = b * a)

## Instances For

A commutative star-ordered ring is an ordered ring.

This is not registered as an instance because it introduces a type class loop between `CommSemiring`

and `OrderedCommSemiring`

, and it seem loops still cause issues sometimes.

See note [reducible non-instances].

## Equations

- StarOrderedRing.toOrderedCommRing R = OrderedCommRing.mk (_ : ā (a b : R), a * b = b * a)