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) = ⊤

instance NNRat.instStarOrderedRing : StarOrderedRing ℚ≥0

Equations

• NNRat.instStarOrderedRing = ⋯

@[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 ℚ

instance Rat.instStarOrderedRing : StarOrderedRing ℚ

Equations

• Rat.instStarOrderedRing = ⋯