[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.[/step]

[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: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.[/step]

[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: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$.[/step]

[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: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.[/step]

[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]