Solution (source code)

= Solution

A <splitting field> of a nonzero <polynomial> $f$ over $K$ is an extension in which $f$ splits into linear factors and which is generated over $K$ by all its roots. For a constant nonzero <polynomial> the <splitting field> is $K$; the zero <polynomial> does not have a root-generated <splitting field> in this standard definition.

Given two <splitting fields> $L,L'$, enumerate the roots generating $L$ and extend a $K$-embedding one root at a time. If an embedding is defined on $K(\alpha_1,\ldots,\alpha_j)$, the <minimal polynomial> of the next root divides $f$ over that <field>. Its image under the embedding therefore divides $f$ over the corresponding subfield of $L'$, and has a root in $L'$. The quotient construction $K(\alpha)\cong K[t]/(m_\alpha)$ extends the embedding to that root. The <polynomial> need not be a <separable polynomial>.

At the end this gives a $K$-embedding $L\to L'$. It sends the distinct roots of $f$ injectively to its roots, hence permutes the finite <set> of distinct roots and contains every root in its image. Since these generate $L'$, the embedding is onto. Thus \b[the <splitting field> is unique up to a (K)-isomorphism].