Documentation

Mathlib.Data.Rat.Star

Star ordered ring structures on and ℚ≥0 #

This file shows that and ℚ≥0 are StarOrderedRings. In particular, this means that every nonnegative rational number is a sum of squares.