Galois extensions of the real numbers

TheoremDegree of a finite extension of the reals#✓fully proved

If \(E\) is a field that is a finite-dimensional algebra over \(\mathbb{R}\), then the dimension of \(E\) as a real vector space is \(1\) or \(2\).

This follows because such a field \(E\) is isomorphic as an \(\mathbb{R}\)-algebra to \(\mathbb{R}\) or to \(\mathbb{C}\).

theorem finrank_eq_one_or_two {E : Type*} [Field E] [Algebra ℝ E]
    [FiniteDimensional ℝ E] :
    Module.finrank ℝ E = 1 ∨ Module.finrank ℝ E = 2

Used by 1

Used byGalois groups over the reals have order 1 or 2

TheoremGalois groups over the reals have order 1 or 2#✓fully proved

If \(E\) is a finite Galois extension of \(\mathbb{R}\), then the Galois group \(\mathrm{Gal}(E/\mathbb{R})\) has order \(1\) or \(2\).

theorem gal_card_eq_one_or_two {E : Type*} [Field E] [Algebra ℝ E]
    [FiniteDimensional ℝ E] [IsGalois ℝ E] :
    Nat.card Gal(E/ℝ) = 1 ∨ Nat.card Gal(E/ℝ) = 2

Uses 1 · Used by 1

Proof usesDegree of a finite extension of the reals

Used byGalois groups over the reals have order a power of 2

TheoremGalois groups over the reals have order a power of 2#✓fully proved

If \(E\) is a finite Galois extension of \(\mathbb{R}\), then the Galois group \(\mathrm{Gal}(E/\mathbb{R})\) has order \(2^n\) for some natural number \(n\).

In fact the order is \(1\) or \(2\).

theorem gal_card_pow_two {E : Type*} [Field E] [Algebra ℝ E]
    [FiniteDimensional ℝ E] [IsGalois ℝ E] :
    ∃ n : ℕ, Nat.card Gal(E/ℝ) = 2 ^ n

Sources

the book's lemma in Lecture 34 (Main Theorem of Algebra).

Uses 1

Proof usesGalois groups over the reals have order 1 or 2

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.