---
tag: 0JZGW75C5Z
kind: statement
role: proposition
name: Power rule
msc: [26A24]
uses: [0F1WR9C83K, 0V9A43H7WV]
sources:
  - url: https://en.wikipedia.org/wiki/Power_rule
    locator: Proof by induction (natural numbers)
same_as:
  wikidata: Q1190543
  wikipedia: 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|0V9A43H7WV]] 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|0KY08TWDMQ]] 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$.