Product rule

Statement

Let $f$ and $g$ be real functions on an open interval $I$, both differentiable at $a \in I$. Then $f g$ is differentiable at $a$, and $$(f g)'(a) = f'(a) g(a) + f(a) g'(a).$$

Remarks

Write $f(a + h) g(a + h) - f(a) g(a) = (f(a + h) - f(a)) g(a + h) + f(a) (g(a + h) - g(a))$. Divide by $h$ and use the continuity of $g$ at $a$. For example, $(x \sin x)' = \sin x + x \cos x$. Mathlib states it as HasDerivAt.mul.

History

The discovery of the rule is credited to Gottfried Leibniz.

Explanations

L1 human

Think of $f g$ as the area of a rectangle with sides $f$ and $g$. When both sides grow a little, the area grows by $f' g + f g'$, up to a tiny corner piece.