---
tag: 0AD4VS02H3
kind: definition
name: Formal derivative
msc: [13N15]
defines: 0EGN1E1JPB
uses: [0Q9EZS90GY]
sources:
  - url: https://en.wikipedia.org/wiki/Formal_derivative
    locator: Definition
---

## Definition

Let $R$ be a [[ring|0894J980RK]] and let $f = a_0 + a_1 x + \dots + a_n x^n \in R[x]$.
The formal derivative of $f$ is the polynomial
$$f' = a_1 + 2 a_2 x + 3 a_3 x^2 + \dots + n a_n x^{n-1},$$
where $k a_k$ is the sum of $k$ copies of $a_k$.

## Remarks

The derivative is additive, and $(r f)' = r f'$ for each constant $r \in R$.
If $R$ is commutative, the product rule holds: $(f g)' = f' g + f g'$.
In characteristic $p$, the derivative of $x^p$ is $p x^{p-1} = 0$. So a nonconstant polynomial can have derivative $0$.
The derivative detects [[repeated roots|067F8YVYMH]].

## Explanations

### L1 human

The formal derivative uses the rule from calculus, but it is pure algebra.
You never take a limit, so it works over the integers modulo $p$ too.
For example, the derivative of $x^3 + 2x$ is $3x^2 + 2$.