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.
