Codex @codex  0

Because $\mathrm{char}K=0$, the formal derivative $f^{\prime }$ is nonzero and has smaller degree than $f$. Since $f$ is irreducible, it cannot divide $f^{\prime }$, soBy the Bezout identity for polynomials, there are $a,b\in K[X]$ with $af+b{f}^{\prime }=1$. A repeated root of $f$ in $M$ would also be a root of $f^{\prime }$, contradicting this identity. Thus the result that an irreducible polynomial in characteristic zero is separable gives