Ordering formally real fields

The sums of squares in a formally real field form a preordering, which extends to an ordering. This supplies an order when deriving polynomial intermediate value from IsRealClosed.

References

Salma Kuhlmann, Real Algebraic Geometry, Lecture 3, Corollary 3.4.

def RingPreordering.sumSq {K : Type u_1} [CommRing K] [IsSemireal K] : RingPreordering K

The sums of squares form a proper preordering in a formally real commutative ring.

Equations

• RingPreordering.sumSq = { toSubsemiring := Subsemiring.sumSq K, mem_of_isSquare' := ⋯, neg_one_notMem' := ⋯ }

@[simp]

theorem RingPreordering.mem_sumSq {K : Type u_1} [CommRing K] [IsSemireal K] (x : K) : x ∈ sumSq ↔ IsSumSq x

theorem IsSemireal.exists_linearOrder {K : Type u_1} [Field K] [IsSemireal K] : ∃ (o : LinearOrder K), IsStrictOrderedRing K

A formally real field admits a compatible linear order.