Star order structure on ℚ

Here we put the trivial star operation on ℚ for convenience and show that it is a StarOrderedRing. In particular, this means that every element of ℚ is a sum of squares.

instance Rat.instStarRingRatToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing : StarRing ℚ

Equations

• One or more equations did not get rendered due to their size.

instance Rat.instTrivialStarRatToStarToInvolutiveStarAddMonoidToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRingInstStarRingRatToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing : TrivialStar ℚ

Equations

• One or more equations did not get rendered due to their size.

instance Rat.instStarOrderedRingRatToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRingInstPartialOrderRat : StarOrderedRing ℚ

Equations

• One or more equations did not get rendered due to their size.