Power rule

Statement

Let $n \ge 1$ be a natural number. Then the function $x \mapsto x^n$ is differentiable on $\mathbb{R}$, and its derivative at $x$ is $n x^{n-1}$.

Remarks

Induction on $n$ with the product rule gives $(x^{n+1})' = (x^n \cdot x)' = n x^{n-1} \cdot x + x^n = (n + 1) x^n$. The same formula holds for negative integers $n$ when $x \ne 0$, and for real exponents when $x > 0$. Mathlib states it as hasDerivAt_pow.

Explanations

L1 human

To differentiate a power, bring the exponent down as a factor and lower the exponent by one. For example, the derivative of $x^5$ is $5 x^4$.