Finite normal extension as a splitting field
= Finite normal extension as a splitting field
A finite extension $L/K$ is <normal field extension>[normal] exactly when it is the splitting field over $K$ of some polynomial. For the forward direction, multiply the minimal polynomials of finitely many generators of $L$; normality puts all their roots in $L$. The reverse direction follows because a $K$-embedding permutes the roots of a polynomial and hence preserves its splitting field.