Galois Extensions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we define Galois extensions as extensions which are both separable and normal.
Main definitions #
Main results #
Together, these two results prove the Galois correspondence.
is_galois.tfae : Equivalent characterizations of a Galois extension of finite degree
A field extension E/F is galois if it is both separable and normal. Note that in mathlib
a separable extension of fields is by definition algebraic.
Instances of this typeclass
Equivalent characterizations of a Galois extension of finite degree