Finite normal extension as a splitting field

A finite extension $L/K$ is 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.