Solution (source code)

= Solution

An <algebraic element> is a <separable algebraic element> over $K$ if its <minimal polynomial of an algebraic element> has distinct roots in a <splitting field>. A <field extension> is a <separable extension> if all its elements are <separable algebraic elements>.

The <formal derivative> is additive and satisfies $D(X^m)=mX^{m-1}$. For monomials, $D(X^rX^s)=(r+s)X^{r+s-1}=X^rD(X^s)+X^sD(X^r)$. Distributing over the finitely many coefficients proves the <product rule> $D(fg)=fDg+gDf$ over any <field>. If $f=(X-\alpha)^2h$ in an extension, the rule gives $Df=2(X-\alpha)h+(X-\alpha)^2Dh$, so $Df(\alpha)=0$, including in <characteristic two>. If $f,Df$ were relatively prime in $K[X]$, the <Bézout's identity for polynomials> would give $uf+vDf=1$, whose evaluation at $\alpha$ is impossible. Hence they are not relatively prime.

In <characteristic zero>, the <formal derivative> of a positive-degree <irreducible polynomial> $m$ is nonzero and has smaller degree. Thus $\gcd(m,Dm)=1$, since an <irreducible polynomial> has no proper nonconstant factor. By the previous argument, $m$ has no repeated root. Every element of a <finite field extension> is algebraic, so the extension is a <separable extension>.

For $K=\mathbb F_p(t)$, let $\alpha^p=t$. The characteristic-$p$ identity gives $X^p-t=(X-\alpha)^p$, so $K(\alpha)$ is already a <splitting field>. It is a proper extension by the allowed no-root fact. More precisely, the <minimal polynomial of an algebraic element> $\alpha$ divides $X^p-t$ and, over $K(\alpha)$, equals $(X-\alpha)^r$ for some $1\le r\le p$. If $r<p$, its next-to-leading coefficient is $-r\alpha\in K$, forcing $\alpha\in K$ because $r\ne0$ in $\mathbb F_p$, a contradiction. Hence its <minimal polynomial of an algebraic element> is $X^p-t$, with its one root repeated $p$ times. The extension is therefore \b[inseparable], of degree $p$.

By contrast, every <finite field extension> $L/\mathbb F_p$ is a <separable extension>. If $[L:\mathbb F_p]=n$, then $|L|=p^n$. <Lagrange's theorem> in its nonzero multiplicative <group> gives $a^{p^n}=a$ for all $a\in L$. Thus every element is a root of $X^{p^n}-X$, whose <formal derivative> is $-1$; it has no repeated roots. Every <minimal polynomial of an algebraic element> divides this separable <polynomial>, proving the assertion.