[proofplan]
We must show that the splitting field $L$ of a separable polynomial $f \in K[t]$ is both normal and separable over $K$. Normality is immediate: by the [Normal Equals Splitting Field](/theorems/1269) characterisation, any splitting field of a polynomial over $K$ is a normal extension of $K$. For separability, we use the [Characterisation of Separable Extensions](/theorems/1265), condition (3): $L = K(\alpha_1, \ldots, \alpha_n)$ where the $\alpha_i$ are the roots of $f$, and each minimal polynomial $P_{\alpha_i, K}$ divides $f$. Since $f$ has no repeated roots and each $P_{\alpha_i, K}$ is an irreducible divisor of $f$, the $P_{\alpha_i, K}$ have no repeated roots either. Hence each generator has separable minimal polynomial, and condition (3) gives that $L/K$ is separable.
[/proofplan]
[step:Establish normality of $L/K$ via the splitting field characterisation]
Let $L$ denote a splitting field of $f$ over $K$. By definition, $f$ splits completely in $L[t]$ and $L$ is generated over $K$ by the roots of $f$. The [Normal Equals Splitting Field](/theorems/1269) theorem states that a finite extension $L/K$ is normal if and only if $L$ is the splitting field of some polynomial in $K[t]$. Since $L$ is the splitting field of $f \in K[t]$, the extension $L/K$ is normal.
[guided]
The first property we must establish is normality of $L/K$. Recall that a finite extension $L/K$ is **normal** if every irreducible polynomial in $K[t]$ that has at least one root in $L$ splits completely over $L$.
Rather than verify this condition directly, we appeal to the [Normal Equals Splitting Field](/theorems/1269) characterisation, which provides the equivalence: a finite extension $L/K$ is normal if and only if $L$ is the splitting field of some polynomial in $K[t]$.
We verify the hypothesis: by assumption, $L$ is the splitting field of $f$ over $K$. This means two things: (i) $f$ splits into linear factors in $L[t]$, and (ii) no proper subfield of $L$ containing $K$ has this property. These are precisely the conditions for $L$ to be a splitting field of $f$ in the sense required by theorem 1269.
Therefore $L/K$ is normal.
Note that we have not used the separability of $f$ in this step. Normality of a splitting field holds regardless of whether $f$ has repeated roots — it depends only on $L$ being generated by the complete set of roots of a polynomial over $K$.
[/guided]
[/step]
[step:Identify the generators of $L/K$ as roots of $f$]
Since $L$ is the splitting field of $f$ over $K$, the polynomial $f$ factors completely in $L[t]$. Write
\begin{align*}
f = c \cdot (t - \alpha_1)(t - \alpha_2) \cdots (t - \alpha_n)
\end{align*}
where $c \in K \setminus \{0\}$ is the leading coefficient, $n = \deg f$, and $\alpha_1, \ldots, \alpha_n \in L$ are the roots of $f$. By the definition of a splitting field, $L = K(\alpha_1, \ldots, \alpha_n)$.
Since $f$ is separable, the roots $\alpha_1, \ldots, \alpha_n$ are pairwise distinct.
[guided]
This step unpacks the definition of a splitting field and the separability hypothesis into the explicit data we need.
By definition, $L$ being a splitting field of $f$ over $K$ means:
1. The polynomial $f$ factors into linear factors in $L[t]$, so we may write $f = c \cdot \prod_{i=1}^{n} (t - \alpha_i)$ with $c \in K \setminus \{0\}$ and $\alpha_1, \ldots, \alpha_n \in L$.
2. The field $L$ is the smallest extension of $K$ in which $f$ splits, i.e., $L = K(\alpha_1, \ldots, \alpha_n)$.
The separability hypothesis on $f$ states that $f$ has no repeated roots in its splitting field. In the factorisation above, this means $\alpha_i \neq \alpha_j$ for all $i \neq j$, i.e., the $n$ roots are pairwise distinct.
Why does this matter for what follows? The key point is that each $\alpha_i$ has a minimal polynomial $P_{\alpha_i, K} \in K[t]$ that divides $f$. If $P_{\alpha_i, K}$ had a repeated root, then $f$ would also have a repeated root (since the roots of $P_{\alpha_i, K}$ are a subset of the roots of $f$). The separability of $f$ therefore propagates to each minimal polynomial.
[/guided]
[/step]
[step:Show each minimal polynomial $P_{\alpha_i, K}$ is separable by divisibility]
Fix $i \in \{1, \ldots, n\}$. The minimal polynomial $P_{\alpha_i, K} \in K[t]$ is the unique monic irreducible polynomial in $K[t]$ with $P_{\alpha_i, K}(\alpha_i) = 0$.
Since $f(\alpha_i) = 0$ and $P_{\alpha_i, K}$ is the minimal polynomial of $\alpha_i$ over $K$, the polynomial $P_{\alpha_i, K}$ divides $f$ in $K[t]$. (This is a standard property: $P_{\alpha_i, K}$ divides every polynomial in $K[t]$ that vanishes at $\alpha_i$, because $P_{\alpha_i, K}$ generates the ideal $\ker(\operatorname{ev}_{\alpha_i}) = \{g \in K[t] : g(\alpha_i) = 0\}$ in the principal ideal domain $K[t]$.)
Write $f = P_{\alpha_i, K} \cdot q_i$ for some $q_i \in K[t]$. In the splitting field $L$, the roots of $P_{\alpha_i, K}$ form a subset of the roots of $f$. Since $f$ has no repeated roots in $L$, neither does $P_{\alpha_i, K}$: if $\beta$ were a repeated root of $P_{\alpha_i, K}$ in $L$, then $\beta$ would appear with multiplicity at least $2$ in the factorisation of $P_{\alpha_i, K}$, and hence with multiplicity at least $2$ in the factorisation of $f = P_{\alpha_i, K} \cdot q_i$ (regardless of whether $q_i(\beta) = 0$), contradicting the separability of $f$.
Therefore $P_{\alpha_i, K}$ has no repeated roots, i.e., $P_{\alpha_i, K}$ is a separable polynomial. Since $i \in \{1, \ldots, n\}$ was arbitrary, every generator $\alpha_i$ of $L$ over $K$ has a separable minimal polynomial over $K$.
[guided]
This is the central step where the separability of $f$ is transferred to each generator's minimal polynomial. The mechanism is divisibility in $K[t]$.
Fix $i \in \{1, \ldots, n\}$ and consider the evaluation homomorphism
\begin{align*}
\operatorname{ev}_{\alpha_i}: K[t] &\to L \\
g &\mapsto g(\alpha_i).
\end{align*}
The kernel $\ker(\operatorname{ev}_{\alpha_i})$ is an ideal in the principal ideal domain $K[t]$, generated by the minimal polynomial $P_{\alpha_i, K}$. Since $f(\alpha_i) = 0$ (because $\alpha_i$ is a root of $f$), we have $f \in \ker(\operatorname{ev}_{\alpha_i})$, so $P_{\alpha_i, K} \mid f$ in $K[t]$.
Now we argue that $P_{\alpha_i, K}$ has no repeated roots. Write $f = P_{\alpha_i, K} \cdot q_i$ in $K[t]$. In the splitting field $L$, both $P_{\alpha_i, K}$ and $q_i$ factor into linear factors. The multiset of roots of $f$ in $L$ is the union (with multiplicity) of the roots of $P_{\alpha_i, K}$ and the roots of $q_i$.
Suppose for contradiction that $P_{\alpha_i, K}$ has a repeated root $\beta \in L$, so that $(t - \beta)^2$ divides $P_{\alpha_i, K}$ in $L[t]$. Then $(t - \beta)^2$ also divides $f = P_{\alpha_i, K} \cdot q_i$ in $L[t]$, so $\beta$ is a repeated root of $f$. This contradicts the hypothesis that $f$ is separable.
Therefore $P_{\alpha_i, K}$ is separable for each $i$.
Why is it important that $P_{\alpha_i, K}$ is irreducible in this argument? Because the divisibility $P_{\alpha_i, K} \mid f$ relies on irreducibility: the minimal polynomial is the generator of the kernel of the evaluation map, and this generator is irreducible. Without irreducibility, we could not conclude that the minimal polynomial divides $f$; we would only know that $f$ lies in the ideal generated by $P_{\alpha_i, K}$, which is the same thing only because $K[t]$ is a PID.
[/guided]
[/step]
[step:Conclude that $L/K$ is separable by the characterisation of separable extensions]
We have shown that $L = K(\alpha_1, \ldots, \alpha_n)$ where each $P_{\alpha_i, K}$ is separable over $K$. By the [Characterisation of Separable Extensions](/theorems/1265), condition (3), a finite extension is separable if and only if it is generated by elements whose minimal polynomials over $K$ are separable. Since condition (3) is satisfied, $L/K$ is a separable extension.
[guided]
The [Characterisation of Separable Extensions](/theorems/1265) provides four equivalent conditions for a finite extension $L/K$ to be separable. Condition (3) states: $L = K(\alpha_1, \ldots, \alpha_n)$ where each minimal polynomial $P_{\alpha_i, K}$ is separable over $K$.
We verify that the hypotheses of the characterisation theorem are met:
- $L/K$ is a finite extension. Indeed, $L = K(\alpha_1, \ldots, \alpha_n)$ where each $\alpha_i$ is algebraic over $K$ (being a root of $f \in K[t]$), so $[L : K] \le \prod_{i=1}^{n} \deg P_{\alpha_i, K} \le (\deg f)^n < \infty$.
- The generators $\alpha_1, \ldots, \alpha_n$ have separable minimal polynomials $P_{\alpha_i, K}$ over $K$, as established in the previous step.
Therefore condition (3) of the characterisation holds, and the equivalence $(3) \Leftrightarrow (2)$ gives that $L/K$ is separable in the sense that every element of $L$ has a separable minimal polynomial over $K$.
Combining the two properties: $L/K$ is both normal (from the first step) and separable (from this step). A finite extension that is both normal and separable is, by definition, a Galois extension. Therefore $L/K$ is Galois.
[/guided]
[/step]