---
tag: 0V9A43H7WV
kind: statement
role: theorem
name: Product rule
aliases: [leibniz-rule-for-products]
msc: [26A24]
uses: [0F1WR9C83K, 07ZMX4ANJS]
sources:
  - url: https://en.wikipedia.org/wiki/Product_rule
    locator: Limit definition of derivative
same_as:
  wikidata: Q466720
  wikipedia: 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$|07ZMX4ANJS]].
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.