[proofplan] The proof treats each direction of the equivalence separately. For the forward direction, we show that if $f \in K[t^p]$, then the formal derivative $Df$ vanishes identically: every monomial $a_k t^{kp}$ differentiates to $kp \cdot a_k t^{kp-1} = 0$ in characteristic $p$. The vanishing of $Df$ forces $\gcd(f, Df) = f \neq 1$, so $f$ has a repeated root by the derivative criterion for repeated roots. For the converse, we show that if $f$ is inseparable, then irreducibility forces $Df = 0$ via a degree comparison: $\gcd(f, Df)$ divides $f$ and is a non-trivial factor, so irreducibility gives $f \mid Df$, but $\deg(Df) < \deg(f)$ unless $Df = 0$. Finally, the vanishing $Df = 0$ in characteristic $p$ means every coefficient $a_k$ with $p \nmid k$ must vanish, which is precisely the condition $f \in K[t^p]$. [/proofplan]

[step:Forward direction: show that $f \in K[t^p]$ implies $Df = 0$, hence $f$ is inseparable] Assume $f \in K[t^p]$. Then there exists a polynomial $g \in K[t]$ such that $f(t) = g(t^p)$. Write \begin{align*} g(t) = \sum_{k=0}^{m} a_k t^k, \quad a_k \in K, \end{align*} so that \begin{align*} f(t) = g(t^p) = \sum_{k=0}^{m} a_k t^{kp}. \end{align*} We compute the formal derivative of $f$. By linearity of the formal derivative and the rule $D(t^j) = j \cdot t^{j-1}$: \begin{align*} Df(t) = \sum_{k=0}^{m} a_k \cdot kp \cdot t^{kp - 1}. \end{align*} Since $\operatorname{char} K = p$, we have $kp = 0$ in $K$ for every integer $k$. Therefore every term in the sum vanishes, giving $Df = 0$. Since $f$ is irreducible, $f$ is non-constant, so $f \neq 0$. The formal derivative $Df = 0$ implies $\gcd(f, Df) = \gcd(f, 0) = f$. In particular, $\gcd(f, Df) \neq 1$. Let $L$ be a splitting field of $f$ over $K$, and write $f(t) = c \prod_{i=1}^{n}(t - \alpha_i)$ in $L[t]$ where $c \in K \setminus \{0\}$ and $\alpha_1, \ldots, \alpha_n \in L$ (listed with multiplicity). By the derivative criterion for repeated roots, $f$ has a repeated root if and only if $\gcd(f, Df) \neq 1$ (where the gcd is computed in $K[t]$, equivalently in $L[t]$ since $K[t]$ is a UFD and the gcd is unchanged by passing to the splitting field). Since $\gcd(f, Df) = f \neq 1$, the polynomial $f$ has a repeated root, i.e., $f$ is inseparable.[/step]

[guided]The goal is to show that any polynomial of the form $g(t^p)$ is automatically inseparable in characteristic $p$. The mechanism is the formal derivative. Recall that the formal derivative \begin{align*} D: K[t] &\to K[t] \\ \sum_{k=0}^{n} a_k t^k &\mapsto \sum_{k=1}^{n} k \cdot a_k t^{k-1} \end{align*} is defined purely algebraically — no limits are involved. It is a $K$-linear map satisfying the product rule $D(fg) = Df \cdot g + f \cdot Dg$. Now, if $f(t) = g(t^p) = \sum_{k=0}^{m} a_k t^{kp}$, then $f$ is a polynomial whose only non-zero terms occur at powers that are multiples of $p$. When we differentiate a monomial $a_k t^{kp}$, we obtain $kp \cdot a_k t^{kp-1}$. But $kp \equiv 0 \pmod{p}$, so in a field of characteristic $p$, the coefficient $kp$ is the zero element of $K$. Every term in $Df$ vanishes, giving $Df = 0$. Why does $Df = 0$ imply inseparability? The connection is the classical criterion: a polynomial $f \in K[t]$ has a repeated root (in some splitting field) if and only if $\gcd(f, Df) \neq 1$. When $Df = 0$, the gcd of $f$ and $Df$ is $\gcd(f, 0) = f$ itself (up to units), which is non-constant since $f$ is irreducible. Hence $\gcd(f, Df) \neq 1$, and $f$ has a repeated root. Note the contrast with characteristic zero: in $\mathbb{Q}[t]$, a non-constant polynomial $f$ always satisfies $Df \neq 0$ (since $\deg(Df) = \deg(f) - 1 \ge 0$ and the leading coefficient is $n \cdot a_n \neq 0$ when $\operatorname{char} K = 0$). The phenomenon $Df = 0$ for $f \neq 0$ is specific to positive characteristic.[/guided]

[step:Converse direction: show that inseparability forces $f \mid Df$, hence $Df = 0$]Assume $f$ is inseparable, i.e., $f$ has a repeated root in some splitting field. By the derivative criterion for repeated roots, $\gcd(f, Df) \neq 1$. Let $d := \gcd(f, Df) \in K[t]$ (computed as a monic gcd in the Euclidean domain $K[t]$). Since $d \mid f$ and $d \neq 1$, the polynomial $d$ is a non-trivial divisor of $f$. Since $f$ is irreducible in $K[t]$, the only monic divisors of $f$ are $1$ and $f/c$ where $c$ is the leading coefficient of $f$ (i.e., the associates of $f$). Since $d \neq 1$, we conclude that $d$ is an associate of $f$, so $f \mid d$. Since $d = \gcd(f, Df)$ divides $Df$, it follows that $f \mid Df$. Now compare degrees. Since $f$ is non-constant (irreducible polynomials have degree at least $1$), we have $\deg(f) \ge 1$. If $Df \neq 0$, then $\deg(Df) = \deg(f) - 1$ (noting that the leading term of $Df$ is $n a_n t^{n-1}$ where $n = \deg(f)$ and $a_n$ is the leading coefficient; if $n a_n = 0$, then $\deg(Df) < \deg(f) - 1$, which only strengthens the argument). In either case, $Df \neq 0$ would give $\deg(Df) < \deg(f)$, contradicting $f \mid Df$ (since a non-zero polynomial divisible by $f$ must have degree at least $\deg(f)$). Therefore $Df = 0$.[/step]

[guided]The goal is to prove the converse: if $f$ is inseparable, then $Df = 0$. The argument uses the interplay between irreducibility and the formal derivative. We begin with the derivative criterion: $f$ has a repeated root if and only if $\gcd(f, Df) \neq 1$. This is a standard result whose proof uses the factorisation of $f$ in a splitting field — if $f(t) = c(t - \alpha)^2 q(t)$, then $Df(t) = c \cdot 2(t-\alpha)q(t) + c(t-\alpha)^2 Dq(t)$, so $(t - \alpha)$ divides both $f$ and $Df$, giving $\gcd(f, Df) \neq 1$. Conversely, if all roots are simple, then $f$ and $Df$ share no root, so $\gcd(f, Df) = 1$. Now, $d := \gcd(f, Df)$ is a divisor of $f$ in $K[t]$ with $d \neq 1$. What are the possible divisors of an irreducible polynomial? By definition, $f$ is irreducible if and only if its only divisors (up to units) are $1$ and $f$ itself. Since $d \neq 1$ and $d \mid f$, we must have $d \sim f$ (where $\sim$ denotes association, i.e., $d = cf$ for some $c \in K \setminus \{0\}$). In particular, $f \mid d$. Since $d = \gcd(f, Df)$ divides $Df$, the divisibility $f \mid d \mid Df$ gives $f \mid Df$. Can $Df$ be non-zero? If $Df \neq 0$, then $Df$ is a non-zero polynomial with $\deg(Df) \le \deg(f) - 1 < \deg(f)$. But $f \mid Df$ and $Df \neq 0$ would require $\deg(Df) \ge \deg(f)$, a contradiction. Therefore $Df = 0$. The key point to appreciate: in characteristic zero, this argument never triggers because an irreducible polynomial always has $\gcd(f, Df) = 1$ (since $Df \neq 0$ and $\deg(Df) = \deg(f) - 1$, so the irreducibility of $f$ prevents $f$ from dividing $Df$). It is only in characteristic $p > 0$ that the formal derivative can vanish, allowing the gcd to be non-trivial.[/guided]

[step:Extract the coefficient condition: $Df = 0$ in characteristic $p$ means $f \in K[t^p]$] Write \begin{align*} f(t) = \sum_{k=0}^{n} a_k t^k, \quad a_k \in K, \quad a_n \neq 0. \end{align*} The formal derivative is \begin{align*} Df(t) = \sum_{k=1}^{n} k \cdot a_k t^{k-1}. \end{align*} The condition $Df = 0$ means that every coefficient of $Df$ vanishes: \begin{align*} k \cdot a_k = 0 \quad \text{for all } k \in \{1, 2, \ldots, n\}. \end{align*} For each index $k$, either $k \cdot 1_K = 0$ in $K$ (i.e., $\operatorname{char}(K) \mid k$, equivalently $p \mid k$) or $k \cdot 1_K \neq 0$ in $K$, in which case $k \cdot 1_K$ is a unit in $K$ and the equation $k \cdot a_k = 0$ forces $a_k = 0$. Therefore: $a_k = 0$ for every $k$ with $p \nmid k$. The only indices $k$ for which $a_k$ can be non-zero are those divisible by $p$, i.e., $k \in \{0, p, 2p, 3p, \ldots\}$. This means \begin{align*} f(t) = \sum_{\substack{k=0 \\ p \mid k}}^{n} a_k t^k = \sum_{j=0}^{\lfloor n/p \rfloor} a_{jp} \, t^{jp} = \sum_{j=0}^{\lfloor n/p \rfloor} a_{jp} \, (t^p)^j. \end{align*} Define \begin{align*} g: K &\to K \\ t &\mapsto \sum_{j=0}^{\lfloor n/p \rfloor} a_{jp} \, t^j, \end{align*} so that $g \in K[t]$ and $f(t) = g(t^p)$. This shows $f \in K[t^p]$.[/step]

[guided]We have established $Df = 0$ in the previous step. The remaining task is to translate the vanishing of the formal derivative into a structural statement about the exponents appearing in $f$. Write $f(t) = \sum_{k=0}^{n} a_k t^k$ with $a_n \neq 0$. The formal derivative is $Df(t) = \sum_{k=1}^{n} k \cdot a_k t^{k-1}$. Since $\{1, t, t^2, \ldots\}$ is a basis for $K[t]$ as a $K$-vector space, the polynomial $Df$ is zero if and only if every coefficient vanishes: $k \cdot a_k = 0$ for $k = 1, 2, \ldots, n$. Now we use the characteristic. In a field $K$ with $\operatorname{char} K = p > 0$, the element $k \cdot 1_K$ (the image of the integer $k$ under the ring homomorphism $\mathbb{Z} \to K$) is zero if and only if $p \mid k$. For indices $k$ with $p \nmid k$, the element $k \cdot 1_K$ is non-zero in $K$, hence a unit (since $K$ is a field). The equation $k \cdot a_k = (k \cdot 1_K) \cdot a_k = 0$ with $k \cdot 1_K$ a unit forces $a_k = 0$. For indices $k$ with $p \mid k$, the equation $k \cdot a_k = 0 \cdot a_k = 0$ is satisfied regardless of the value of $a_k$. These are the indices where a non-zero coefficient is permitted. The conclusion: the polynomial $f$ has the form $f(t) = a_0 + a_p t^p + a_{2p} t^{2p} + \cdots$, i.e., $f$ is a polynomial in $t^p$. Setting $g(t) := a_0 + a_p t + a_{2p} t^2 + \cdots = \sum_{j=0}^{\lfloor n/p \rfloor} a_{jp} t^j$, we have $f(t) = g(t^p)$ and $g \in K[t]$, so $f \in K[t^p]$. Combining both directions: $f$ is inseparable $\implies$ $Df = 0$ (by the previous step) $\implies$ $f \in K[t^p]$ (by the analysis above). Together with the forward direction, we have the equivalence: $f$ is inseparable if and only if $f \in K[t^p]$.[/guided]