Power rule
Builds on DerivativeProduct rule
Statement
Let be a natural number. Then the function is differentiable on , and its derivative at is .
Remarks
Induction on with the product rule gives .
The same formula holds for negative integers when , and for real exponents when .
Mathlib states it as hasDerivAt_pow.
Reading path
To understand this page from the ground up, read these 8 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Limit point of a set definition
- Limit of a function definition
- Continuity at a point definition
- Derivative definition
- Differentiable function definition
- Differentiable functions are continuous statement
- Product rule statement
- Power rule statement
Where this leads
3 pages build on this one.
Further reading
- Web https://en.wikipedia.org/wiki/Power_rule, Proof by induction (natural numbers)
About this page
| Tag | 0JZGW75C5Z |
|---|---|
| URI | m2://0JZGW75C5Z |
| Kind | statement, proposition |
| Writing | W1 stated |
| MSC | 26A24 |
| Status | This copy of the site has no build data. Run m2 status 0JZGW75C5Z. |
| Uses | Derivative, Product rule |
| Same as |
Markdown · JSON · Edit on GitHub
What this page needs for W2
- edge about out: the concepts that the statement is about (0 of 1)
- edge proves in: at least one proof node (0 of 1)
- edge instance_of or illustrates in: one example that shows the statement at work (0 of 1)
- explanation L2 (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.