Commit 2023-09-07 00:04 6079a14f

refactor(FieldTheory/NormalClosure): change definition and add API (#6163) This PR adds API and changes the definition of the normal closure of $F\leq K\leq L$ to be an intermediate field of L/F, rather than an intermediate field of L/K. For example, I think it would be more common to say that the normal closure of $\mathbb{Q}(\sqrt[3]{2})/\mathbb{Q}$ is $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}$ rather than $\mathbb{Q}(\sqrt[3]{2},\zeta_3)/\mathbb{Q}(\sqrt[3]{2})$. This change also means that the normal closure goes from being a dependent function (K : Type) → IntermediateField K L to being a non-dependent function Type → IntermediateField F L, making it easier to compare across the Galois corespondence. Supersedes https://github.com/leanprover-community/mathlib/pull/18971