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.

The real numbers are shown to form a real closed field in Mathlib/Analysis/Polynomial/IsRealClosed.lean.

TODO (Artie Khovanov) : equivalent conditions for a real field to be real closed TODO (Artie Khovanov) : 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