Real Closed Field

A field R is real closed if all of the following hold:

1. R is real (that is, -1 is not a sum of squares in R).
2. for every x in R, one of x or -x is a square.
3. every odd-degree polynomial over R has a root in R.

A real closed field is an algebraic generalisation of the real numbers.

In this file we define real closed fields and prove some of their properties.

TODO (Artie Khovanov) : equivalent conditions for a real field to be real closed TODO (Artie Khovanov) : real numbers, real algebraic numbers, hyperreals form a real closed field

Main Definitions

• IsRealClosed R is the typeclass saying R is a real closed field.

Tags

real closed, rcf

class IsRealClosed (R : Type u_1) [Field R] extends IsSemireal R : Prop

A field R is real closed if all of the following hold:

1. R is real (that is, -1 is not a sum of squares in R).
2. for every x in R, one of x or -x is a square.
3. every odd-degree polynomial over R has a root in R.

• one_add_ne_zero {s : R} (hs : IsSumSq s) : 1 + s ≠ 0
• isSquare_or_isSquare_neg (x : R) : IsSquare x ∨ IsSquare (-x)
• exists_isRoot_of_odd_natDegree {f : Polynomial R} (hf : Odd f.natDegree) : ∃ (x : R), f.IsRoot x

theorem IsRealClosed.of_linearOrderedField {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x) (exists_isRoot_of_odd_natDegree : ∀ {f : Polynomial R}, Odd f.natDegree → ∃ (x : R), f.IsRoot x) : IsRealClosed R

theorem IsSquare.of_not_isSquare_neg {R : Type u} [Field R] [IsRealClosed R] {x : R} (hx : ¬IsSquare (-x)) : IsSquare x

theorem IsRealClosed.isSquare_neg_of_not_isSquare {R : Type u} [Field R] [IsRealClosed R] {x : R} (hx : ¬IsSquare x) : IsSquare (-x)

theorem IsRealClosed.exists_eq_pow_of_odd {R : Type u} [Field R] [IsRealClosed R] (x : R) {n : ℕ} (hn : Odd n) : ∃ (r : R), x = r ^ n

theorem IsRealClosed.exists_eq_zpow_of_odd {R : Type u} [Field R] [IsRealClosed R] (x : R) {k : ℤ} (hk : Odd k) : ∃ (r : R), x = r ^ k

theorem IsRealClosed.exists_eq_pow_of_isSquare {R : Type u} [Field R] [IsRealClosed R] {x : R} (hx : IsSquare x) {n : ℕ} (hn : n ≠ 0) : ∃ (r : R), x = r ^ n

theorem IsRealClosed.exists_eq_zpow_of_isSquare {R : Type u} [Field R] [IsRealClosed R] {x : R} (hx : IsSquare x) {k : ℤ} (hk : k ≠ 0) : ∃ (r : R), x = r ^ k

theorem IsRealClosed.nonneg_iff_isSquare {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} : 0 ≤ x ↔ IsSquare x

theorem IsSquare.of_nonneg {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} : 0 ≤ x → IsSquare x

Alias of the forward direction of IsRealClosed.nonneg_iff_isSquare.

theorem IsRealClosed.exists_eq_pow_of_nonneg {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ x) {n : ℕ} (hn : n ≠ 0) : ∃ (r : R), x = r ^ n

theorem IsRealClosed.exists_eq_zpow_of_nonneg {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ x) {k : ℤ} (hk : k ≠ 0) : ∃ (r : R), x = r ^ k