[proofplan]
We work in the algebraic closure $\overline{k}$ where $f$ splits completely. If $f$ has a repeated root $\alpha$, we show $(x - \alpha)$ divides both $f$ and $f'$, so $\gcd(f, f') \ne 1$. Conversely, if $\gcd(f, f') \ne 1$, we extract a common root from a nontrivial common factor and show it must be a repeated root of $f$. The key tool is the product rule for formal derivatives applied to the factorisation $f = (x - \alpha)^m g$ in $\overline{k}[x]$.
[/proofplan]
[step:Factor $f$ in $\overline{k}[x]$ and compute $f'$ via the product rule]
Since $\overline{k}$ is algebraically closed, $f$ splits completely in $\overline{k}[x]$. Let $\alpha \in \overline{k}$ be a root of $f$ with multiplicity $m \geq 1$, so that
\begin{align*}
f(x) = (x - \alpha)^m g(x)
\end{align*}
for some $g \in \overline{k}[x]$ with $g(\alpha) \ne 0$. Applying the product rule for formal derivatives:
\begin{align*}
f'(x) = m(x - \alpha)^{m-1} g(x) + (x - \alpha)^m g'(x) = (x - \alpha)^{m-1}\bigl[m \cdot g(x) + (x - \alpha) g'(x)\bigr].
\end{align*}
[guided]
The formal derivative $f'$ of a polynomial $f = \sum_{i=0}^n a_i x^i \in k[x]$ is defined purely algebraically as $f' = \sum_{i=1}^n i \cdot a_i x^{i-1}$, where $i \cdot a_i$ denotes the $i$-fold sum $a_i + \cdots + a_i$ in $k$. No limit or convergence is involved — this is an operation on the ring $k[x]$. The product rule $(fg)' = f'g + fg'$ holds in any polynomial ring by a direct verification on monomials.
Since $\overline{k}$ is algebraically closed, $f$ factors completely over $\overline{k}$. Fix a root $\alpha \in \overline{k}$ of $f$ and write $f(x) = (x - \alpha)^m g(x)$ where $m \geq 1$ is the multiplicity of $\alpha$ and $g \in \overline{k}[x]$ satisfies $g(\alpha) \ne 0$. Applying the product rule:
\begin{align*}
f'(x) &= \frac{d}{dx}\bigl[(x - \alpha)^m\bigr] \cdot g(x) + (x - \alpha)^m \cdot g'(x) \\
&= m(x - \alpha)^{m-1} g(x) + (x - \alpha)^m g'(x) \\
&= (x - \alpha)^{m-1}\bigl[m \cdot g(x) + (x - \alpha) g'(x)\bigr].
\end{align*}
The factored form makes the multiplicity of $\alpha$ as a root of $f'$ visible: the factor $(x - \alpha)^{m-1}$ is always present, and the bracketed expression may or may not vanish at $\alpha$.
[/guided]
[/step]
[step:Show that a repeated root of $f$ is a common root of $f$ and $f'$]
Suppose $\alpha$ is a repeated root, i.e., $m \geq 2$. Then $(x - \alpha)^{m-1}$ divides $f'(x)$, and since $m - 1 \geq 1$, we have $f'(\alpha) = 0$. Since also $f(\alpha) = 0$, the polynomial $(x - \alpha)$ divides both $f$ and $f'$ in $\overline{k}[x]$.
Now, the Euclidean algorithm computes $\gcd(f, f')$ using only divisions in $k[x]$ (since $f, f' \in k[x]$), so $d := \gcd(f, f') \in k[x]$. Since $(x - \alpha)$ divides both $f$ and $f'$ in $\overline{k}[x]$, it divides any $k[x]$-linear combination of $f$ and $f'$, hence it divides $d$ in $\overline{k}[x]$. In particular $\deg d \geq 1$, so $\gcd(f, f') \ne 1$.
[guided]
Suppose $\alpha$ is a repeated root of $f$, meaning $m \geq 2$. From the factorisation of $f'$ in the previous step, $(x - \alpha)^{m-1}$ divides $f'$, and $m - 1 \geq 1$ ensures $f'(\alpha) = 0$. So $\alpha$ is a common root of $f$ and $f'$ in $\overline{k}$.
Why does a common root in $\overline{k}$ force the gcd in $k[x]$ to be nontrivial? The Euclidean algorithm for $\gcd(f, f')$ performs only polynomial long divisions with coefficients in $k$ (both $f$ and $f'$ lie in $k[x]$), producing a sequence of remainders in $k[x]$. The last nonzero remainder is $d = \gcd(f, f') \in k[x]$. By Bézout's identity in $k[x]$, there exist $a, b \in k[x]$ with $af + bf' = d$. In $\overline{k}[x]$, the element $(x - \alpha)$ divides both $f$ and $f'$, so $(x - \alpha) \mid d$ in $\overline{k}[x]$. This forces $\deg d \geq 1$, hence $\gcd(f, f') \ne 1$ in $k[x]$.
[/guided]
[/step]
[step:Show that a nontrivial $\gcd(f, f')$ forces a repeated root]
Conversely, suppose $d := \gcd(f, f') \ne 1$ in $k[x]$, so $\deg d \geq 1$. Since $d \in k[x]$ has positive degree, it has a root $\alpha \in \overline{k}$. Then $\alpha$ is a root of both $f$ and $f'$.
Write $f(x) = (x - \alpha)^m g(x)$ with $g(\alpha) \ne 0$ and $m \geq 1$. From the derivative computation:
\begin{align*}
f'(\alpha) = 0 \cdot \bigl[m \cdot g(\alpha) + 0\bigr] + \text{terms with } (x-\alpha) = m \cdot g(\alpha) \cdot (\alpha - \alpha)^{m-1}.
\end{align*}
More precisely, evaluating $f'(\alpha) = (x - \alpha)^{m-1}[m \cdot g(x) + (x - \alpha)g'(x)]$ at $x = \alpha$: if $m = 1$, then $f'(\alpha) = 1 \cdot g(\alpha) = g(\alpha) \ne 0$, contradicting $f'(\alpha) = 0$. Therefore $m \geq 2$, and $\alpha$ is a repeated root of $f$.
[guided]
For the converse, assume $\gcd(f, f') \ne 1$, meaning the gcd has degree at least $1$. Let $d = \gcd(f, f') \in k[x]$. Since $\deg d \geq 1$, the polynomial $d$ has at least one root $\alpha$ in $\overline{k}$ (every nonconstant polynomial over a field has a root in the algebraic closure). Since $d \mid f$ and $d \mid f'$ in $k[x]$, we have $f(\alpha) = 0$ and $f'(\alpha) = 0$.
We need to show $\alpha$ is a repeated root of $f$, i.e., $m \geq 2$ in the factorisation $f(x) = (x - \alpha)^m g(x)$ with $g(\alpha) \ne 0$. Suppose for contradiction that $m = 1$. Then $f(x) = (x - \alpha)g(x)$ and the product rule gives $f'(x) = g(x) + (x - \alpha)g'(x)$. Evaluating at $x = \alpha$:
\begin{align*}
f'(\alpha) = g(\alpha) + 0 = g(\alpha) \ne 0,
\end{align*}
contradicting $f'(\alpha) = 0$. Therefore $m \geq 2$, and $\alpha$ is a repeated root of $f$.
[/guided]
[/step]
[step:Conclude the separability criterion]
Combining the two directions: $f$ has a repeated root in $\overline{k}$ if and only if $\gcd(f, f') \ne 1$ in $k[x]$. Taking the contrapositive, $f$ has no repeated roots in $\overline{k}$ — i.e., $f$ is separable — if and only if $\gcd(f, f') = 1$ in $k[x]$.
[/step]
