[proofplan] We prove both directions of the equivalence by working in the splitting field $L$. For the forward direction, if $\alpha \in L$ is a repeated root of $f$, we factor $f = (t - \alpha)^m g$ with $m \ge 2$ and compute $Df(\alpha) = 0$ via the product rule, showing $(t - \alpha)$ divides both $f$ and $Df$ in $L[t]$, hence $\gcd(f, Df) \neq 1$ in $L[t]$. Since $\gcd(f, Df)$ can be computed in $K[t]$ by the Euclidean algorithm (and is unchanged upon passing to $L[t]$), the gcd is non-trivial in $K[t]$ as well. For the converse, if $\gcd(f, Df) \neq 1$ in $K[t]$, then $f$ and $Df$ share a common root $\alpha$ in $L$. Writing $f = (t - \alpha)^m g$ with $g(\alpha) \neq 0$ and computing $Df(\alpha)$, the assumption $m = 1$ forces the contradiction $Df(\alpha) = g(\alpha) \neq 0$, so $m \ge 2$. [/proofplan] [step:Forward direction: factor $f$ at a repeated root and compute $Df(\alpha) = 0$ via the product rule] Assume $f$ has a repeated root $\alpha \in L$. Then $\alpha$ has multiplicity $m \ge 2$ in $f$, meaning there exists a polynomial $g \in L[t]$ such that \begin{align*} f = (t - \alpha)^m g, \quad g(\alpha) \neq 0. \end{align*} We compute the formal derivative of $f$ using the product rule for formal derivatives in $L[t]$. The product rule gives \begin{align*} Df = D\bigl((t - \alpha)^m\bigr) \cdot g + (t - \alpha)^m \cdot Dg = m(t - \alpha)^{m-1} g + (t - \alpha)^m Dg. \end{align*} Factoring out $(t - \alpha)^{m-1}$: \begin{align*} Df = (t - \alpha)^{m-1}\bigl(m g + (t - \alpha) Dg\bigr). \end{align*} Since $m \ge 2$, we have $m - 1 \ge 1$, so $(t - \alpha)$ divides $Df$ in $L[t]$. Since $(t - \alpha)$ also divides $f = (t - \alpha)^m g$, it follows that $(t - \alpha)$ divides $\gcd(f, Df)$ in $L[t]$, and in particular $\gcd(f, Df) \neq 1$ in $L[t]$. [guided] We are given that $\alpha$ is a repeated root, meaning $\alpha$ appears with multiplicity $m \ge 2$ in the factorisation of $f$ over $L$. Since $L$ is a splitting field of $f$ over $K$, the polynomial $f$ splits completely in $L[t]$, and we may write $f = (t - \alpha)^m g$ where $g \in L[t]$ satisfies $g(\alpha) \neq 0$ (the factor $(t - \alpha)$ has been extracted exactly $m$ times). We need the formal derivative. Recall that the formal derivative $D: L[t] \to L[t]$ is the unique $L$-linear map satisfying $D(t^k) = k t^{k-1}$ for all $k \ge 0$. It obeys the product rule $D(pq) = Dp \cdot q + p \cdot Dq$ for all $p, q \in L[t]$ (this is verified by checking on monomials and extending by linearity). Applying the product rule to $f = (t - \alpha)^m \cdot g$: \begin{align*} Df &= D\bigl((t - \alpha)^m\bigr) \cdot g + (t - \alpha)^m \cdot Dg. \end{align*} For the first term, we compute $D\bigl((t - \alpha)^m\bigr)$. Since $\alpha \in L$ is a constant, $(t - \alpha)^m = \sum_{k=0}^{m} \binom{m}{k} (-\alpha)^{m-k} t^k$, and the formal derivative gives $D\bigl((t - \alpha)^m\bigr) = m(t - \alpha)^{m-1}$ (this follows from the chain rule for formal derivatives, or by direct computation using the binomial expansion). Substituting: \begin{align*} Df &= m(t - \alpha)^{m-1} g + (t - \alpha)^m Dg \\ &= (t - \alpha)^{m-1}\bigl(mg + (t - \alpha)Dg\bigr). \end{align*} Since $m \ge 2$, the factor $(t - \alpha)^{m-1}$ has degree at least $1$, so $(t - \alpha)$ divides $Df$ in $L[t]$. Now, $(t - \alpha)$ divides both $f$ and $Df$ in $L[t]$, so it divides their gcd: $(t - \alpha) \mid \gcd(f, Df)$ in $L[t]$. In particular, $\gcd(f, Df) \neq 1$ in $L[t]$. Why does this give us information in $K[t]$? This is addressed in the next step. [/guided] [/step] [step:Lift the non-trivial gcd from $L[t]$ to $K[t]$ using compatibility of the Euclidean algorithm with field extensions] The polynomials $f$ and $Df$ both have coefficients in $K$ (the formal derivative of a polynomial in $K[t]$ has coefficients in $K$, since $D(\sum a_k t^k) = \sum k a_k t^{k-1}$ and each $k a_k \in K$). The Euclidean algorithm computes $\gcd(f, Df)$ by performing successive polynomial divisions, each involving only arithmetic operations in the coefficient field. Therefore the Euclidean algorithm applied to $f, Df$ in $K[t]$ produces exactly the same sequence of quotients and remainders as when applied in $L[t]$ (since $K \subset L$ and the operations agree). In particular, $\gcd(f, Df)$ computed in $K[t]$ and $\gcd(f, Df)$ computed in $L[t]$ are associates (they differ by a unit in the respective rings). Since $\gcd(f, Df) \neq 1$ in $L[t]$ (as shown in the previous step), we conclude $\gcd(f, Df) \neq 1$ in $K[t]$. [guided] This step addresses a subtlety that is easy to overlook. The factorisation $f = (t - \alpha)^m g$ was performed in $L[t]$, and we showed that $(t - \alpha) \mid \gcd(f, Df)$ in $L[t]$. But the theorem statement asserts $\gcd(f, Df) \neq 1$ in $K[t]$, so we must relate the two gcds. The key fact is that the Euclidean algorithm is purely algebraic: given $f, Df \in K[t]$, the algorithm produces a sequence of remainders $r_1, r_2, \ldots$ by polynomial long division, using only addition, subtraction, multiplication, and division by leading coefficients -- all of which are operations within $K$. Therefore every remainder $r_i$ lies in $K[t]$, and the final non-zero remainder (the gcd) lies in $K[t]$. Now, if we run the same algorithm viewing $f, Df$ as elements of $L[t]$, the divisions proceed identically, because the operations in $K$ are a subset of the operations in $L$. The same sequence of quotients and remainders is produced. In particular, the monic gcd is the same polynomial whether computed in $K[t]$ or $L[t]$. Since $\gcd(f, Df) \neq 1$ in $L[t]$ (it is divisible by $(t - \alpha)$), the gcd is a polynomial in $K[t]$ of degree at least $1$. This completes the forward direction. [/guided] [/step] [step:Converse direction: a non-trivial gcd forces $f$ and $Df$ to share a common root in $L$] Conversely, assume $\gcd(f, Df) \neq 1$ in $K[t]$. Let $d := \gcd(f, Df) \in K[t]$, which has $\deg d \ge 1$ by assumption. Since $d \mid f$ in $K[t]$ and $f$ splits completely in $L$ (because $L$ is a splitting field of $f$ over $K$), every irreducible factor of $d$ over $K$ has a root in $L$. In particular, $d$ has a root $\alpha \in L$. Since $d \mid f$ and $d \mid Df$, the element $\alpha$ is a common root of $f$ and $Df$ in $L$: \begin{align*} f(\alpha) = 0 \quad \text{and} \quad Df(\alpha) = 0. \end{align*} [guided] We assume $\gcd(f, Df) \neq 1$ in $K[t]$ and must produce a repeated root of $f$ in $L$. Since $\gcd(f, Df)$ is a polynomial in $K[t]$ of degree at least $1$, it has at least one irreducible factor $h \in K[t]$ with $\deg h \ge 1$. Since $h \mid \gcd(f, Df) \mid f$ and $f$ splits completely over $L$ (by definition of splitting field), the polynomial $h$ has at least one root $\alpha$ in $L$. Since $h \mid \gcd(f, Df)$, we have $h \mid f$ and $h \mid Df$. Evaluating at $\alpha$: $f(\alpha) = 0$ (because $h(\alpha) = 0$ and $h \mid f$) and $Df(\alpha) = 0$ (because $h(\alpha) = 0$ and $h \mid Df$). The existence of a common root of $f$ and $Df$ is the critical input for the next step, where we show this forces $\alpha$ to have multiplicity at least $2$ in $f$. [/guided] [/step] [step:Show the common root has multiplicity at least $2$ by computing $Df(\alpha)$ in terms of the multiplicity] Since $f$ splits completely in $L[t]$ and $f(\alpha) = 0$, we may write \begin{align*} f = (t - \alpha)^m g \end{align*} for some integer $m \ge 1$ and polynomial $g \in L[t]$ with $g(\alpha) \neq 0$ (here $m$ is the exact multiplicity of $\alpha$ as a root of $f$). Applying the product rule for formal derivatives as in the forward direction: \begin{align*} Df = (t - \alpha)^{m-1}\bigl(mg + (t - \alpha)Dg\bigr). \end{align*} Evaluating at $t = \alpha$: \begin{align*} Df(\alpha) = (\alpha - \alpha)^{m-1}\bigl(m g(\alpha) + (\alpha - \alpha)Dg(\alpha)\bigr) = 0^{m-1} \cdot m g(\alpha). \end{align*} We consider two cases based on $m$. **Case $m = 1$.** Then $0^{m-1} = 0^0 = 1$, so $Df(\alpha) = 1 \cdot 1 \cdot g(\alpha) = g(\alpha) \neq 0$. This contradicts $Df(\alpha) = 0$ established in the previous step. **Case $m \ge 2$.** Then $0^{m-1} = 0$, so $Df(\alpha) = 0$, which is consistent. Since $m = 1$ leads to a contradiction, we conclude $m \ge 2$. Therefore $\alpha$ is a repeated root of $f$ in $L$. [guided] We have $f(\alpha) = 0$ and $Df(\alpha) = 0$ from the previous step, and we must show $\alpha$ has multiplicity at least $2$. Since $L$ is a splitting field of $f$, the polynomial $f$ factors completely as a product of linear factors in $L[t]$. Collecting all factors of $(t - \alpha)$, we write $f = (t - \alpha)^m g$ where $m \ge 1$ is the exact multiplicity of $\alpha$ and $g \in L[t]$ satisfies $g(\alpha) \neq 0$. The product rule gives: \begin{align*} Df &= m(t - \alpha)^{m-1} g + (t - \alpha)^m Dg \\ &= (t - \alpha)^{m-1}\bigl(mg + (t - \alpha)Dg\bigr). \end{align*} Evaluating at $t = \alpha$, the factor $(t - \alpha)Dg$ vanishes regardless of $Dg(\alpha)$, and we obtain: \begin{align*} Df(\alpha) = 0^{m-1} \cdot mg(\alpha). \end{align*} Now, suppose for contradiction that $m = 1$. Then $0^{m-1} = 0^0 = 1$ (the empty product), so \begin{align*} Df(\alpha) = 1 \cdot 1 \cdot g(\alpha) = g(\alpha). \end{align*} Since $g(\alpha) \neq 0$ (by the choice of $m$ as the exact multiplicity), this gives $Df(\alpha) = g(\alpha) \neq 0$. But we established $Df(\alpha) = 0$ in the previous step, a contradiction. Therefore $m \ge 2$, and $\alpha$ is a repeated root of $f$ in $L$. It is worth noting what each hypothesis contributed. The splitting field assumption ensured that every factor of $\gcd(f, Df)$ has a root in $L$, providing the common root $\alpha$. The properties of the formal derivative (the product rule and the computation $D(t - \alpha)^m = m(t - \alpha)^{m-1}$) translated the vanishing of $Df(\alpha)$ into the algebraic constraint $m \ge 2$ on the multiplicity. [/guided] [/step]