Formal derivative of a polynomial

Definition

Suppose $K$ is a field and $f(x)\in K[x]$ is a polynomial. The formal derivative of $f$, denoted $f'$, is defined as follows.

If $f(x)=\sum _{m=0}^{n}a_{m}x^{m}$, then $f'(x)=\sum _{m=1}^{n}ma_{m}x^{m-1}$.

Here, the $ma_{m}$ is understood as $a_{m}$ added to itself $m$ times.

Facts

The formal derivative gives a $K$-linear map from $K[x]$ to itself. When $K$ has characteristic zero, the kernel of the map is $K$, whereas when $K$ has characteristic $p$, the kernel of the map is $K[x^{p}]$.

The formal derivative also satisfies the following rule for multiplication, called the Leibniz rule:

$\!(fg)'(x)=f'(x)g(x)+f(x)g'(x)$.