As is well-known, every extension of a characteristic zero field is separable and the proof goes by noticing that an irreducible polynomial $f(x)$ has no common root with its formal derivative $Df(x)$.
However, to my intuition, formal derivative seems not a purely algebraic thing. I'm wondering if there is another way to prove this fact, without using formal derivative?
Or is there another angle to view this proof using formal derivative, to illustrate the intuition to use formal derivative?
(What I've come up with is that for $f(x)=\prod\limits_{i=1}^n (x-x_i)$, $Df(x)$ can be viewed as $\sum\limits_{i=1}^n \left(\prod\limits_{j\neq i}(x-x_j)\right)$, which is symmetric in $x_1,\cdots,x_n$ and takes value $0$ on multiple roots of $f(x)$. That is, to prove $f(x)$ is separable, only needs to construct a polynomial that is both symmetric in $x_1,\cdots,x_n$ and takes value $0$ on multiple roots of $f(x)$.)
I wonder is there a proof without formal derivative or a better way to comprehend the proof using formal derivative. Thanks in advance!