Commit 2020-11-27 09:16 2bda184a

feat(field_theory): Prove the Galois correspondence (#4786) The proof leverages existing results from field_theory/fixed.lean and field_theory/primitive_element.lean. We define Galois as normal + separable. Proving the various equivalent characterizations of Galois extensions is yet to be done.