Finite extensions of an abstract real closed field

Odd-degree finite extensions of a real closed field are trivial. A field of characteristic different from two in which every element is a square has no quadratic extension. These are the degree reductions used by the Sylow argument in Galois.lean.

References

The odd-degree and quadratic-extension steps of the Artin–Schreier argument; see Salma Kuhlmann, Real Algebraic Geometry, Lecture 5, Theorem 2.2.

theorem TauCeti.RealClosure.finrank_eq_one_of_odd {R : Type u_1} {E : Type u_2} [Field R] [IsRealClosed R] [Field E] [Algebra R E] [FiniteDimensional R E] (h : Odd (Module.finrank R E)) : Module.finrank R E = 1

An odd-degree finite extension of a real closed field is trivial.

theorem TauCeti.RealClosure.finrank_ne_two_of_forall_isSquare {K : Type u_3} {L : Type u_4} [Field K] [NeZero 2] [Field L] [Algebra K L] (hsq : ∀ (x : K), IsSquare x) : Module.finrank K L ≠ 2

A square-closed field of characteristic different from two has no quadratic extension.