Normal closure of subfield exists and is finite dimensional

Stream: Is there code for X?

[Sebastian Monnet]

I'm trying to prove that, given a field extension $L/K$ and a finite subextension $E/K$, there is some finite subextension $N/K$ such that every conjugate of fixing_subgroup E (i.e. $Gal(L/E)$) is contained in fixing_subgroup N (i.e. $Gal(L/N)$). Clearly the right choice for $N$ is the normal closure of $E$ in $L$, but I can't find it in mathlib.

Does the normal closure exist somewhere? If it does, do we have that the normal closure of a finite extension is finite?

[Thomas Browning]

If you're assuming separable (which you might be, since you seem to be doing Galois theory), then you could adjoin the roots of a primitive element, which will automatically be normal and finite dimensional.

[Kevin Buzzard]

I don't think we need separable here. You could adjoin the roots of the min polys of a basis. Might be icky though.