[proofplan] Let $f \in K[t]$ be irreducible with $\operatorname{char} K = 0$. We show $f$ is separable by proving $\gcd(f, Df) = 1$, then invoking the [Repeated Root Criterion](/theorems/1261). The argument has two ingredients: first, the characteristic-zero hypothesis forces the formal derivative $Df$ to be a nonzero polynomial (its leading term is $n \cdot a_n t^{n-1}$, where $n \ge 1$ and $n \neq 0$ in $K$). Second, the irreducibility of $f$ combined with the strict degree inequality $\deg Df < \deg f$ forces $\gcd(f, Df) = 1$. [/proofplan] [step:Compute the formal derivative $Df$ and verify it is nonzero] Let $n := \deg f \ge 1$ (an irreducible polynomial has degree at least $1$). Write \begin{align*} f = a_n t^n + a_{n-1} t^{n-1} + \cdots + a_1 t + a_0 \in K[t], \end{align*} where $a_n \neq 0$. The formal derivative of $f$ is \begin{align*} Df = n \cdot a_n \, t^{n-1} + (n-1) \cdot a_{n-1} \, t^{n-2} + \cdots + 1 \cdot a_1. \end{align*} We claim $Df \neq 0$. The leading term of $Df$ is $n \cdot a_n \, t^{n-1}$. Since $a_n \neq 0$ (as the leading coefficient of $f$) and $n \ge 1$, it suffices to show that $n \cdot a_n \neq 0$ in $K$. In a field of characteristic zero, the ring homomorphism $\mathbb{Z} \to K$ defined by $1 \mapsto 1_K$ is injective: for every positive integer $m$, the element $m \cdot 1_K = \underbrace{1_K + \cdots + 1_K}_{m} \neq 0$. Applying this with $m = n$, we obtain $n \cdot 1_K \neq 0$, and therefore $n \cdot a_n = (n \cdot 1_K) \cdot a_n \neq 0$ since $K$ is a field and $a_n \neq 0$. Hence $Df$ is a nonzero polynomial with $\deg Df = n - 1$. [/step] [step:Conclude $\gcd(f, Df) = 1$ from irreducibility and the degree bound] Let $d := \gcd(f, Df) \in K[t]$. Since $d \mid f$ and $f$ is irreducible in $K[t]$, the only monic divisors of $f$ are $1$ and $f / a_n$ (the monic associate of $f$). Therefore either $d = 1$ or $d$ is an associate of $f$, which means either $\gcd(f, Df) = 1$ or $f \mid Df$. The second alternative is impossible: $Df \neq 0$ (established above), so $Df$ has a well-defined degree $\deg Df = n - 1$. If $f \mid Df$, then $\deg f \le \deg Df$, giving $n \le n - 1$, a contradiction. Therefore $\gcd(f, Df) = 1$. [guided] This step is where the irreducibility hypothesis does its work. In $K[t]$, which is a principal ideal domain, the greatest common divisor $d = \gcd(f, Df)$ is defined up to units (nonzero scalars in $K$). Since $d \mid f$, we know $f = d \cdot q$ for some $q \in K[t]$. Now we use irreducibility. An irreducible element of $K[t]$ has no factorisation $f = d \cdot q$ with both $d$ and $q$ non-units. So either $d$ is a unit (i.e., $d \in K \setminus \{0\}$, which means $\gcd(f, Df) = 1$) or $q$ is a unit (i.e., $d$ is an associate of $f$, which means $f \mid \gcd(f, Df)$, and since $\gcd(f, Df) \mid Df$, this forces $f \mid Df$). Why is $f \mid Df$ impossible? Because the formal derivative strictly lowers the degree: $\deg Df = n - 1 < n = \deg f$. A nonzero polynomial cannot be divisible by a polynomial of larger degree in $K[t]$. (If $Df = f \cdot h$ for some $h \in K[t]$, then $\deg Df = \deg f + \deg h \ge \deg f$, contradicting $n - 1 < n$.) Note that this argument requires $Df \neq 0$. If $Df$ were the zero polynomial, then $f \mid Df$ would hold vacuously (since $f \mid 0$ for any $f$), and we could not rule out the second alternative. This is precisely the failure mode in characteristic $p > 0$: an irreducible polynomial $f \in K[t^p]$ satisfies $Df = 0$, so $\gcd(f, Df) = f \neq 1$, and $f$ has repeated roots. [/guided] [/step] [step:Apply the Repeated Root Criterion to conclude separability] By the [Repeated Root Criterion](/theorems/1261), a polynomial $f \in K[t]$ has a repeated root in its splitting field over $K$ if and only if $\gcd(f, Df) \neq 1$ in $K[t]$. We have established $\gcd(f, Df) = 1$, so $f$ has no repeated roots. By definition, this means $f$ is separable. [/step]