Theorems · Theorem · field theory

IsGalois.card_aut_eq_finrank

∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  [IsGalois F E], Nat.card Gal(E/F) = Module.finrank F E

Let $E / F$ be a finite extension of fields. If $E$ is Galois over $F$, then $|\text{Aut}(E/F)| = [E : F]$.

Defined in

Mathlib.FieldTheory.Galois.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensionalIsGalois