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

A real closure of an ordered field is a real closed ordered algebraic extension.

• 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
• 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

Sufficient conditions to be real closed

theorem IsRealClosed.of_isAdjoinRoot_i_or_finrank_eq_one {R : Type u} [Field R] (hR : ¬IsSquare (-1)) (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_isAlgClosure {R : Type u} [Field R] {K : Type u_1} [Field K] [Algebra R K] [IsAlgClosure R K] (h : IsAdjoinRootMonic' K (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.of_maximal_isSemireal {R : Type u} [Field R] [IsSemireal R] (h : ∀ (K : Type u) [inst : Field K] [IsSemireal K] [inst_2 : Algebra R K] [Algebra.IsAlgebraic R K], Module.finrank R K = 1) : IsRealClosed R

theorem IsSquare.of_isSumSq {R : Type u} [Field R] [IsRealClosed R] {x : R} (hx : IsSumSq x) : IsSquare x

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

Classification of algebraic extensions of a real closed field

theorem IsRealClosed.odd_finrank_extension (R : Type u) [Field 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] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [Algebra.IsQuadraticExtension R K] : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)

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

theorem IsRealClosed.isSquare_of_isAdjoinRoot_i (R : Type u) [Field 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] [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] [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] [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] [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_realClosedField (R : Type u) [Field R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [Algebra.IsAlgebraic R K] : FiniteDimensional R K

theorem IsRealClosed.maximal_isSemireal (R : Type u) [Field R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [IsSemireal K] [Algebra.IsAlgebraic R K] : Module.finrank R K = 1

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

instance IsRealClosed.instIsQuadraticExtensionOfIsAlgClosure_realClosedField (R : Type u) [Field 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] [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] [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] [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] [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.irred_poly_natDegree {R : Type u} [Field R] [IsRealClosed R] {f : Polynomial R} (hf : Irreducible f) : f.natDegree ≤ 2

@[instance_reducible]

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

Equations

• IsRealClosed.unique_isStrictOrderedRing R = IsSemireal.unique_isStrictOrderedRing ⋯

theorem IsRealClosed.intermediate_value_property {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing 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

theorem IsRealClosed.TFAE (R : Type u) [Field R] : [IsRealClosed R, IsAdjoinRootMonic' (AlgebraicClosure R) (Polynomial.X ^ 2 + 1), IsSemireal R ∧ ∀ (K : Type u) [inst : Field K] [IsSemireal K] [inst_2 : Algebra R K] [Algebra.IsAlgebraic R K], Module.finrank R K = 1].TFAE

theorem IsRealClosed.TFAE_linearOrderedField (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] : [IsRealClosed R, ∀ (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, ∀ {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 weak_Artin_Schreier {R : Type u_1} [Field R] (hR_char : ringChar R ≠ 2) (hR : Module.finrank R (AlgebraicClosure R) = 2) : IsRealClosed R

theorem Artin_Schreier {R : Type u_1} [Field R] (hR : FiniteDimensional R (AlgebraicClosure R)) : IsRealClosed R