class IsRealClosed (R : Type u_1) [Field R] [LinearOrder R] [IsStrictOrderedRing R] : Prop

• isSquare_of_nonneg {x : R} (hx : 0 ≤ x) : IsSquare x
• exists_isRoot_of_odd_natDegree {f : Polynomial R} (hf : Odd f.natDegree) : ∃ (x : R), f.IsRoot x

class IsRealClosure (K : Type u_1) (R : Type u_2) [Field K] [Field R] [LinearOrder K] [LinearOrder R] [Algebra K R] [IsStrictOrderedRing R] [IsStrictOrderedRing K] extends IsRealClosed R, IsOrderedModule K R, Algebra.IsAlgebraic K R : Prop

• isSquare_of_nonneg {x : R} (hx : 0 ≤ x) : IsSquare x
• exists_isRoot_of_odd_natDegree {f : Polynomial R} (hf : Odd f.natDegree) : ∃ (x : R), f.IsRoot x
• smul_le_smul_of_nonneg_left ⦃a : K⦄ (ha : 0 ≤ a) ⦃b₁ b₂ : R⦄ (hb : b₁ ≤ b₂) : a • b₁ ≤ a • b₂
• smul_le_smul_of_nonneg_right ⦃b : R⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : K⦄ (ha : a₁ ≤ a₂) : a₁ • b ≤ a₂ • b
• isAlgebraic (x : R) : IsAlgebraic K x

theorem IsRealClosed.isSquare_or_isSquare_neg {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (x : R) : IsSquare x ∨ IsSquare (-x)

noncomputable def IsRealClosed.unique_isStrictOrderedRing (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] : Unique { l : LinearOrder R // IsStrictOrderedRing R }

Equations

• IsRealClosed.unique_isStrictOrderedRing R = { default := ⟨inferInstance, ⋯⟩, uniq := ⋯ }

instance IsRealClosed.instFactIrreduciblePolynomialHAddHPowXOfNat {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] : Fact (Irreducible (Polynomial.X ^ 2 + 1))

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

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

Classification of algebraic extensions of a real closed field

theorem IsRealClosed.odd_finrank_extension (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] [FiniteDimensional R K] (hK : Odd (Module.finrank R K)) : Module.finrank R K = 1

theorem IsRealClosed.isAdjoinRoot_i_of_isQuadraticExtension (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [Algebra.IsQuadraticExtension R K] : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)

theorem IsRealClosed.isSquare_of_isAdjoinRoot_i (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) (x : K) : IsSquare x

theorem IsRealClosed.finrank_neq_two_of_isAdjoinRoot_i (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) (L : Type u_2) [Field L] [Algebra K L] : Module.finrank K L ≠ 2

theorem IsRealClosed.finite_extension_rank_le (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [FiniteDimensional R K] : Module.finrank R K ≤ 2

theorem IsRealClosed.rank_eq_one_of_isAdjoinRoot_i (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) (L : Type u_2) [Field L] [Algebra R L] [Algebra K L] [FiniteDimensional R L] [IsScalarTower R K L] : Module.finrank K L = 1

theorem IsRealClosed.finite_extension_classify (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [FiniteDimensional R K] : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1) ∨ Module.finrank R K = 1

instance IsRealClosed.instFiniteDimensionalOfIsAlgebraic (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [Algebra.IsAlgebraic R K] : FiniteDimensional R K

theorem IsRealClosed.maximal_isOrderedField (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [LinearOrder K] [IsOrderedRing K] [Algebra.IsAlgebraic R K] : Module.finrank R K = 1

theorem IsRealClosed.isAdjoinRoot_i_of_isAlgClosure (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [IsAlgClosure R K] : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)

instance IsRealClosed.instIsQuadraticExtensionOfIsAlgClosure (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] [IsAlgClosure R K] : Algebra.IsQuadraticExtension R K

theorem IsRealClosed.isAlgClosure_iff_isAdjoinRoot_i {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] : IsAlgClosure R K ↔ IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)

theorem IsRealClosed.isAlgClosure_of_isAdjoinRoot_i (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) : IsAlgClosure R K

theorem IsRealClosed.isAlgClosure_of_finrank_ne_one (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] [Algebra.IsAlgebraic R K] (hK : Module.finrank R K ≠ 1) : IsAlgClosure R K

theorem IsRealClosed.irred_poly_classify {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {f : Polynomial R} (hf : f.Monic) : Irreducible f ↔ f.natDegree = 1 ∨ ∃ (a : R) (b : R), b ≠ 0 ∧ f = (Polynomial.X - Polynomial.C a) ^ 2 + Polynomial.C b ^ 2

theorem IsRealClosed.intermediate_value_property {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {f : Polynomial R} {x y : R} (hle : x ≤ y) (hx : 0 ≤ Polynomial.eval x f) (hy : Polynomial.eval y f ≤ 0) : ∃ z ∈ Set.Icc x y, Polynomial.eval z f = 0

Sufficient conditions to be real closed

theorem IsRealClosed.of_isAdjoinRoot_i_or_finrank_eq_one {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (h : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K] [FiniteDimensional R K], IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1) ∨ Module.finrank R K = 1) : IsRealClosed R

theorem IsRealClosed.of_isAdjoinRoot_i_algebraicClosure {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (h : IsAdjoinRootMonic' (AlgebraicClosure R) (Polynomial.X ^ 2 + 1)) : IsRealClosed R

theorem IsRealClosed.of_intermediateValueProperty {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (h : ∀ {f : Polynomial R} {x y : R}, x ≤ y → 0 ≤ Polynomial.eval x f → Polynomial.eval y f ≤ 0 → ∃ z ∈ Set.Icc x y, Polynomial.eval z f = 0) : IsRealClosed R

theorem IsRealClosed.of_maximal_isOrderedAlgebra {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (h : ∀ (K : Type u) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : Algebra R K] [Algebra.IsAlgebraic R K] [IsOrderedModule R K], Module.finrank R K = 1) : IsRealClosed R

theorem IsRealClosed.TFAE (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] : [IsRealClosed R, IsAdjoinRootMonic' (AlgebraicClosure R) (Polynomial.X ^ 2 + 1), ∀ (K : Type u) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : Algebra R K] [Algebra.IsAlgebraic R K] [IsOrderedModule R K], Module.finrank R K = 1, ∀ (K : Type u) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : Algebra R K] [Algebra.IsAlgebraic R K], Module.finrank R K = 1, ∀ {f : Polynomial R} {x y : R}, x ≤ y → 0 ≤ Polynomial.eval x f → Polynomial.eval y f ≤ 0 → ∃ z ∈ Set.Icc x y, Polynomial.eval z f = 0].TFAE

theorem IsSemireal.of_isAdjoinRoot_i_algebraicClosure {R : Type u_1} [Field R] (hR : IsAdjoinRootMonic' (AlgebraicClosure R) (Polynomial.X ^ 2 + 1)) : IsSemireal R

theorem IsSemireal.TFAE_RCF {F : Type u} [Field F] : [IsSemireal F ∧ (∀ (x : F), IsSquare x ∨ IsSquare (-x)) ∧ ∀ {f : Polynomial F}, Odd f.natDegree → ∃ (x : F), f.IsRoot x, IsAdjoinRootMonic' (AlgebraicClosure F) (Polynomial.X ^ 2 + 1), IsSemireal F ∧ ∀ (K : Type u) [inst : Field K] [IsSemireal K] [inst_2 : Algebra F K] [Algebra.IsAlgebraic F K], Module.finrank F K = 1].TFAE

theorem very_weak_Artin_Schreier {R : Type u_1} [Field R] (hR : IsAdjoinRootMonic' (AlgebraicClosure R) (Polynomial.X ^ 2 + 1)) : ∃! l : LinearOrder R, ∃ (x : IsStrictOrderedRing R), IsRealClosed R

theorem weak_Artin_Schreier {R : Type u_1} [Field R] (hR_char : ringChar R ≠ 2) (hR : Module.finrank R (AlgebraicClosure R) = 2) : ∃! l : LinearOrder R, ∃ (x : IsStrictOrderedRing R), IsRealClosed R

theorem Artin_Schreier {R : Type u_1} [Field R] (hR : FiniteDimensional R (AlgebraicClosure R)) : IsAlgClosed R ∨ ∃! l : LinearOrder R, ∃ (x : IsStrictOrderedRing R), IsRealClosed R