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.
@[simp]
theorem
NNRat.addSubmonoid_closure_range_pow
{n : ℕ}
(hn₀ : n ≠ 0)
:
AddSubmonoid.closure (Set.range fun (x : ℚ≥0) => x ^ n) = ⊤
@[simp]
theorem
NNRat.addSubmonoid_closure_range_mul_self :
AddSubmonoid.closure (Set.range fun (x : ℚ≥0) => x * x) = ⊤
@[simp]
theorem
Rat.addSubmonoid_closure_range_pow
{n : ℕ}
(hn₀ : n ≠ 0)
(hn : Even n)
:
AddSubmonoid.closure (Set.range fun (x : ℚ) => x ^ n) = AddSubmonoid.nonneg ℚ
@[simp]
theorem
Rat.addSubmonoid_closure_range_mul_self :
AddSubmonoid.closure (Set.range fun (x : ℚ) => x * x) = AddSubmonoid.nonneg ℚ