General Leibniz rule

Statement

Let $n$ be a natural number, and let $f$ and $g$ be $n$ times differentiable real functions on an open interval $I$. Then $f g$ is $n$ times differentiable on $I$, and $$(f g)^{(n)} = \sum_{k=0}^{n} \binom{n}{k} f^{(k)} g^{(n-k)}.$$

Remarks

The proof is an induction on $n$ with the product rule, like the proof of the binomial theorem. For $n = 1$ it is the product rule. For $n = 2$ it is $(f g)'' = f'' g + 2 f' g' + f g''$. Mathlib states it as iteratedDeriv_mul.

Explanations

L1 human

The rule for the $n$-th derivative of a product looks like the binomial formula for $(a + b)^n$. Each term distributes $n$ differentiations between the two factors.