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.
Mathlib.Data.Rat.Star
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.