Theorems · Theorem · field theory

IsGalois.of_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],
  Nat.card Gal(E/F) = Module.finrank F E → IsGalois F E

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

Defined in

Mathlib.FieldTheory.Galois.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensional