Normal subextension criterion (source code)

= Normal subextension criterion

For a finite Galois extension $L/K$ with group $G$, an intermediate extension $E/K$ is normal exactly when its corresponding subgroup $\operatorname{Gal}(L/E)$ is a <normal subgroup> of $G$.