Documentation

Mathlib.Algebra.Order.Ring.Star

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.

@[reducible, inline]

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
Instances For
    @[reducible, inline]

    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
    Instances For