Documentation

Mathlib.Data.Rat.Star

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.

source
instance Rat.instStarRingRatToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToStrictOrderedRingInstLinearOrderedRingRat :
StarRing ℚ
source
instance Rat.instTrivialStarRatToStarToInvolutiveStarAddMonoidToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToStrictOrderedRingInstLinearOrderedRingRatInstStarRingRatToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToStrictOrderedRingInstLinearOrderedRingRat :
TrivialStar ℚ
source
instance Rat.instStarOrderedRingRatToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRingInstPartialOrderRat :
StarOrderedRing ℚ