Theorems · Definition · field theory

IsGalois.normalBasis

(K : Type u_1) →
  (L : Type u_2) →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : 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.

Defined in

Mathlib.FieldTheory.Galois.NormalBasis

Cited by

1 results in Mathlib

Foundations

Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraFiniteDimensionalIsGalois