Documentation

Mathlib.FieldTheory.Galois.NormalBasis

The normal basis theorem #

We prove the normal basis theorem IsGalois.normalBasis: every finite Galois extension has a basis that is an orbit under the Galois group action.

The proof follows [Cona] Keith Conrad, Linear Independence of Characters.

source
theorem exists_linearIndependent_algEquiv_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] :
∃ (x : L), LinearIndependent K fun (σ : Gal(L/K)) => σ x
source
noncomputable def IsGalois.normalBasis (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] :
Module.Basis Gal(L/K) K L

Given a finite Galois extension L/K, normalBasis K L is a basis of L over K that is an orbit under the Galois group action.

Equations
Instances For
    source
    theorem IsGalois.normalBasis_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (e : Gal(L/K)) :
    (normalBasis K L) e = e ((normalBasis K L) 1)