[proofplan]
We show that every irreducible polynomial over a finite field has no repeated roots, hence every algebraic extension is separable. The key tool is the characterisation of inseparability: an irreducible polynomial $f$ over a field of characteristic $p > 0$ is inseparable if and only if $f(t) = g(t^p)$ for some polynomial $g$. We show this forces $f$ to be a $p$-th power in $K[t]$, contradicting irreducibility. The crucial input is that the Frobenius endomorphism $x \mapsto x^p$ is surjective on any finite field — being an injective map from a finite set to itself.
[/proofplan]
[step:Set up the field and recall the characterisation of inseparable irreducible polynomials]
Let $K = \mathbb{F}_q$ where $q = p^d$ for a prime $p$ and a positive integer $d$. Let $L/K$ be an algebraic extension. To show that $L/K$ is separable, it suffices to show that every irreducible polynomial $f \in K[t]$ is separable — that is, $f$ has no repeated roots in an algebraic closure $\bar{K}$.
An irreducible polynomial $f \in K[t]$ is inseparable if and only if its formal derivative satisfies $f' = 0$ in $K[t]$. Since $\operatorname{char}(K) = p > 0$, the condition $f' = 0$ holds precisely when $f$ is a polynomial in $t^p$: there exists $g \in K[t]$ such that
\begin{align*}
f(t) = g(t^p).
\end{align*}
We will show that this leads to a contradiction with the irreducibility of $f$.
[guided]
Why does $f' = 0$ imply $f(t) = g(t^p)$? Write $f(t) = \sum_{k=0}^n a_k t^k$. Then $f'(t) = \sum_{k=1}^n k \, a_k \, t^{k-1}$. The condition $f' = 0$ means $k \, a_k = 0$ in $K$ for every $k \geq 1$. In characteristic $p$, the integer $k$ is zero in $K$ if and only if $p \mid k$. So $a_k = 0$ whenever $p \nmid k$ (since for such $k$, the coefficient $k$ is a unit in $K$ and $k \, a_k = 0$ forces $a_k = 0$). The only surviving terms are those where $k$ is a multiple of $p$, giving $f(t) = \sum_{j=0}^m a_{jp} \, t^{jp}$, which is $g(t^p)$ where $g(t) = \sum_{j=0}^m a_{jp} \, t^j$.
Conversely, if $f$ is separable, then $\gcd(f, f') = 1$ (since $f$ is irreducible and $f' \neq 0$ means $\deg f' < \deg f$, so $f \nmid f'$, and irreducibility of $f$ forces $\gcd(f, f') = 1$). This means $f$ has no repeated roots. So proving $f' \neq 0$ for every irreducible $f \in K[t]$ of degree $\geq 1$ is equivalent to proving separability.
[/guided]
[/step]
[step:Show that the Frobenius endomorphism is surjective on $K$]
Define the Frobenius map
\begin{align*}
\varphi \colon K &\to K \\
x &\mapsto x^p.
\end{align*}
This is a field homomorphism: $\varphi(xy) = (xy)^p = x^p y^p = \varphi(x)\varphi(y)$, and $\varphi(x + y) = (x + y)^p = x^p + y^p = \varphi(x) + \varphi(y)$ (using the Frobenius endomorphism identity in characteristic $p$, which relies on the fact that the binomial coefficient $\binom{p}{k}$ is divisible by $p$ for $1 \leq k \leq p - 1$).
Since $\varphi$ is a field homomorphism from $K$ to $K$ and $K \neq \{0\}$, the map $\varphi$ is injective ($\ker \varphi = \{0\}$ because $x^p = 0$ implies $x = 0$ in a field). Since $K$ is a finite set and $\varphi \colon K \to K$ is an injective function from a finite set to itself, it is surjective.
Therefore, every element of $K$ is a $p$-th power: for each $a \in K$, there exists $b \in K$ with $b^p = a$.
[guided]
This is the heart of the argument, and it is exactly where the hypothesis that $K$ is *finite* is consumed. The surjectivity of $\varphi$ fails for infinite fields of characteristic $p$: for example, in the rational function field $\mathbb{F}_p(s)$, the element $s$ has no $p$-th root (if $s = (h(s)/g(s))^p$ for polynomials $h, g$, then $s \cdot g(s)^p = h(s)^p$, which gives $\deg(1 + p \deg g) = p \deg h$, a contradiction since $p \nmid 1$). This is precisely why inseparable extensions *can* arise over infinite fields of positive characteristic but *cannot* arise over finite fields.
The argument uses only the pigeonhole principle in the form "an injective self-map of a finite set is surjective." No structural information about $K$ beyond finiteness and the fact that it is a field of characteristic $p$ is required.
[/guided]
[/step]
[step:Deduce that $f(t) = g(t^p)$ implies $f$ is a $p$-th power, contradicting irreducibility]
Suppose for contradiction that $f \in K[t]$ is irreducible and inseparable. By the first step, $f(t) = g(t^p)$ for some $g \in K[t]$. Write
\begin{align*}
g(t) = \sum_{k=0}^m a_k \, t^k,
\end{align*}
so that
\begin{align*}
f(t) = g(t^p) = \sum_{k=0}^m a_k \, t^{pk}.
\end{align*}
By the surjectivity of the Frobenius established in the previous step, for each coefficient $a_k \in K$ there exists $b_k \in K$ such that $b_k^p = a_k$. Substituting, we obtain
\begin{align*}
f(t) &= \sum_{k=0}^m b_k^p \, t^{pk} = \sum_{k=0}^m (b_k \, t^k)^p.
\end{align*}
In characteristic $p$, the Frobenius identity $(x + y)^p = x^p + y^p$ extends by induction to any finite sum: $(\sum_{k=0}^m c_k)^p = \sum_{k=0}^m c_k^p$. Applying this with $c_k = b_k \, t^k$, we obtain
\begin{align*}
f(t) = \sum_{k=0}^m (b_k \, t^k)^p = \left( \sum_{k=0}^m b_k \, t^k \right)^p = g_0(t)^p,
\end{align*}
where $g_0(t) := \sum_{k=0}^m b_k \, t^k \in K[t]$.
Since $\deg g_0 = m$ and $\deg f = pm$, the polynomial $g_0$ satisfies $1 \leq \deg g_0 < \deg f$ (as $p \geq 2$ and $m \geq 1$, the latter because $f$ is inseparable and hence has $\deg f \geq p \geq 2$). The factorisation $f = g_0^p$ expresses $f$ as a product of polynomials of strictly smaller degree, contradicting the irreducibility of $f$.
[guided]
Let us spell out why the Frobenius identity extends to finite sums. We prove by induction on $r$ that in a commutative ring of characteristic $p$,
\begin{align*}
\left( \sum_{k=0}^r c_k \right)^p = \sum_{k=0}^r c_k^p.
\end{align*}
The base case $r = 1$ is the identity $(c_0 + c_1)^p = c_0^p + c_1^p$, which holds because $\binom{p}{j} \equiv 0 \pmod{p}$ for $1 \leq j \leq p - 1$. For the inductive step, set $S = \sum_{k=0}^{r-1} c_k$. Then
\begin{align*}
\left( \sum_{k=0}^r c_k \right)^p = (S + c_r)^p = S^p + c_r^p = \sum_{k=0}^{r-1} c_k^p + c_r^p = \sum_{k=0}^r c_k^p,
\end{align*}
using the base case for $(S + c_r)^p = S^p + c_r^p$ and the inductive hypothesis for $S^p = \sum_{k=0}^{r-1} c_k^p$.
Why does $f = g_0^p$ contradict irreducibility? An irreducible polynomial, by definition, has degree $\geq 1$ and cannot be written as a product of two polynomials each of degree $\geq 1$. Since $g_0^p = g_0 \cdot g_0^{p-1}$ and $\deg g_0 \geq 1$, $\deg g_0^{p-1} = (p-1)m \geq 1$, both factors have positive degree. This is a genuine factorisation into polynomials of smaller degree, which is impossible for an irreducible polynomial.
Note that we have not merely shown that a *particular* irreducible polynomial is separable — the argument applies uniformly to *every* irreducible polynomial in $K[t]$. Since an element $\alpha \in L$ is separable over $K$ precisely when its minimal polynomial over $K$ is separable (i.e., has no repeated roots), and the minimal polynomial is irreducible, we conclude that every element of $L$ is separable over $K$. Hence $L/K$ is separable.
[/guided]
[/step]