[proofplan] We prove two equivalences. First, for an irreducible $f$, inseparability is equivalent to $f' = 0$: this follows from the [Separability via Formal Derivative](/theorems/3329) criterion and the fact that $\gcd(f, f')$ is forced to be $1$ or (an associate of) $f$ when $f$ is irreducible. Second, the condition $f' = 0$ is equivalent to $\operatorname{char}(k) = p > 0$ and $f$ being a polynomial in $x^p$: this is a direct computation with the formal derivative formula $(\sum a_i x^i)' = \sum i \cdot a_i x^{i-1}$. [/proofplan] [step:Show that inseparability of an irreducible polynomial is equivalent to $f' = 0$] Since $f$ is irreducible and nonconstant, its only monic divisors in $k[x]$ are $1$ and $f/\operatorname{lc}(f)$ (where $\operatorname{lc}(f)$ is the leading coefficient). Let $d = \gcd(f, f')$. Since $d \mid f$ and $f$ is irreducible, either $d \sim 1$ (i.e., $\gcd(f, f') = 1$) or $d \sim f$ (i.e., $f \mid f'$). By the [Separability via Formal Derivative](/theorems/3329) criterion, $f$ is inseparable if and only if $\gcd(f, f') \ne 1$, which means $f \mid f'$. But $\deg f' \leq \deg f - 1 < \deg f$ (when $f' \ne 0$), so $f \mid f'$ with $f' \ne 0$ is impossible on degree grounds. Therefore $f \mid f'$ forces $f' = 0$. Conversely, if $f' = 0$, then $\gcd(f, f') = \gcd(f, 0) = f \ne 1$ (since $\deg f \geq 1$), so $f$ is inseparable by the [Separability via Formal Derivative](/theorems/3329) criterion. [guided] Since $f$ is irreducible over $k$, the only divisors of $f$ in $k[x]$ (up to units) are $1$ and $f$ itself. The greatest common divisor $d = \gcd(f, f')$ divides $f$, so there are exactly two cases: either $d \sim 1$ or $d \sim f$. By the [Separability via Formal Derivative](/theorems/3329) criterion, $f$ is inseparable (has a repeated root in $\overline{k}$) if and only if $\gcd(f, f') \ne 1$. In the irreducible case, $\gcd(f, f') \ne 1$ means $f \mid f'$. Now consider what $f \mid f'$ implies about $f'$. The formal derivative of a polynomial of degree $n$ has degree at most $n - 1$ (it has degree exactly $n - 1$ when $n \cdot \operatorname{lc}(f) \ne 0$ in $k$). If $f' \ne 0$, then $\deg f' \leq \deg f - 1 < \deg f$, making $f \mid f'$ impossible since a nonzero polynomial cannot be divisible by a polynomial of strictly larger degree. Therefore $f \mid f'$ forces $f' = 0$ identically. The converse is immediate: if $f' = 0$, then $\gcd(f, f') = \gcd(f, 0) = f$, and since $f$ is nonconstant ($\deg f \geq 1$), we have $\gcd(f, f') \ne 1$, so $f$ is inseparable. [/guided] [/step] [step:Show that $f' = 0$ implies $\operatorname{char}(k) = p > 0$] Write $f(x) = \sum_{i=0}^{n} a_i x^i$ with $a_n \ne 0$ and $n = \deg f \geq 1$. The formal derivative is \begin{align*} f'(x) = \sum_{i=1}^{n} i \cdot a_i \, x^{i-1}, \end{align*} where $i \cdot a_i$ denotes the $i$-fold sum of $a_i$ in $k$. If $f' = 0$, then $i \cdot a_i = 0$ for all $1 \leq i \leq n$. In particular, taking $i = n$: $n \cdot a_n = 0$ with $a_n \ne 0$. In a field, $a_n$ is a unit, so $n \cdot 1_k = 0$ in $k$. This means $\operatorname{char}(k) \ne 0$ (in characteristic $0$, $n \cdot 1_k = 0$ implies $n = 0$, contradicting $n \geq 1$). Let $p = \operatorname{char}(k) > 0$. [guided] Write $f(x) = a_n x^n + a_{n-1} x^{n-1} + \cdots + a_0$ with $a_n \ne 0$ and $n \geq 1$ (since $f$ is nonconstant). The formal derivative formula gives $f'(x) = \sum_{i=1}^n i \cdot a_i x^{i-1}$, where $i \cdot a_i$ means adding $a_i$ to itself $i$ times in $k$. If $f' = 0$ identically, then each coefficient $i \cdot a_i = 0$ for $1 \leq i \leq n$. The leading term gives $n \cdot a_n = 0$. Since $a_n \ne 0$ and $k$ is a field (hence an integral domain), we need $n \cdot 1_k = 0$ in $k$. In characteristic $0$, $n \cdot 1_k \ne 0$ for all $n \geq 1$ (by embedding $\mathbb{Z} \hookrightarrow k$ with trivial kernel), giving a contradiction. Therefore $\operatorname{char}(k) = p$ for some prime $p > 0$. [/guided] [/step] [step:Show that $f' = 0$ in characteristic $p$ is equivalent to $f(x) = g(x^p)$] Continuing with $\operatorname{char}(k) = p > 0$, the condition $f' = 0$ means $i \cdot a_i = 0$ for all $1 \leq i \leq n$. For each such $i$, either $a_i = 0$ or $p \mid i$ (since $k$ has characteristic $p$, the element $i \cdot 1_k = 0$ iff $p \mid i$). Therefore $a_i = 0$ whenever $p \nmid i$. This means $f$ involves only powers of $x$ whose exponents are divisible by $p$: \begin{align*} f(x) = a_0 + a_p x^p + a_{2p} x^{2p} + \cdots + a_{mp} x^{mp} \end{align*} where $mp = n$. Defining $g(t) = a_0 + a_p t + a_{2p} t^2 + \cdots + a_{mp} t^m \in k[t]$, we have $f(x) = g(x^p)$. Conversely, if $f(x) = g(x^p)$ for some $g \in k[x]$ and $\operatorname{char}(k) = p > 0$, write $g(t) = \sum_{j=0}^{m} b_j t^j$. Then $f(x) = \sum_{j=0}^{m} b_j x^{jp}$ and \begin{align*} f'(x) = \sum_{j=1}^{m} jp \cdot b_j \, x^{jp - 1} = 0, \end{align*} since $jp \cdot b_j = j \cdot (p \cdot b_j) = j \cdot 0 = 0$ in $k$ (as $p \cdot 1_k = 0$ in characteristic $p$). [guided] We now characterise polynomials with identically zero derivative in characteristic $p > 0$. The condition $f' = 0$ requires $i \cdot a_i = 0$ for each $1 \leq i \leq n$. In a field of characteristic $p$, the element $i \cdot 1_k$ equals $0$ if and only if $p \mid i$, and $i \cdot 1_k$ is a unit otherwise. So for indices $i$ with $p \nmid i$, the equation $i \cdot a_i = 0$ forces $a_i = 0$ (multiplying both sides by the inverse of $i \cdot 1_k$). For indices $i$ with $p \mid i$, the equation $i \cdot a_i = 0$ holds automatically regardless of $a_i$. The upshot: $f$ can have nonzero coefficients only at positions $0, p, 2p, 3p, \ldots$, giving \begin{align*} f(x) = a_0 + a_p x^p + a_{2p} x^{2p} + \cdots + a_{mp} x^{mp}. \end{align*} This is precisely $f(x) = g(x^p)$ where $g(t) = a_0 + a_p t + a_{2p} t^2 + \cdots + a_{mp} t^m$. For the converse, suppose $\operatorname{char}(k) = p > 0$ and $f(x) = g(x^p) = \sum_{j=0}^m b_j x^{jp}$. Differentiating term by term: \begin{align*} f'(x) = \sum_{j=1}^m (jp) \cdot b_j \, x^{jp-1}. \end{align*} Each coefficient $(jp) \cdot b_j = j \cdot (p \cdot b_j)$. Since $p \cdot 1_k = 0$ in characteristic $p$, we have $p \cdot b_j = 0$ for all $b_j \in k$, so every coefficient vanishes and $f' = 0$. [/guided] [/step] [step:Assemble the two equivalences] Combining the results of the preceding steps: for an irreducible $f \in k[x]$, \begin{align*} f \text{ is inseparable} &\iff f' = 0 \\ &\iff \operatorname{char}(k) = p > 0 \text{ and } f(x) = g(x^p) \text{ for some } g \in k[x]. \end{align*} [/step]