# mathlib3documentation

analysis.calculus.deriv.pow

# Derivative of (f x) ^ n, n : ℕ#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that (x ^ n)' = n * x ^ (n - 1), where n is a natural number.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

## Keywords #

derivative, power

### Derivative of x ↦ x^n for n : ℕ#

theorem has_strict_deriv_at_pow {𝕜 : Type u} (n : ) (x : 𝕜) :
has_strict_deriv_at (λ (x : 𝕜), x ^ n) (n * x ^ (n - 1)) x
theorem has_deriv_at_pow {𝕜 : Type u} (n : ) (x : 𝕜) :
has_deriv_at (λ (x : 𝕜), x ^ n) (n * x ^ (n - 1)) x
theorem has_deriv_within_at_pow {𝕜 : Type u} (n : ) (x : 𝕜) (s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), x ^ n) (n * x ^ (n - 1)) s x
theorem differentiable_at_pow {𝕜 : Type u} {x : 𝕜} (n : ) :
(λ (x : 𝕜), x ^ n) x
theorem differentiable_within_at_pow {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (n : ) :
(λ (x : 𝕜), x ^ n) s x
theorem differentiable_pow {𝕜 : Type u} (n : ) :
(λ (x : 𝕜), x ^ n)
theorem differentiable_on_pow {𝕜 : Type u} {s : set 𝕜} (n : ) :
(λ (x : 𝕜), x ^ n) s
theorem deriv_pow {𝕜 : Type u} {x : 𝕜} (n : ) :
deriv (λ (x : 𝕜), x ^ n) x = n * x ^ (n - 1)
@[simp]
theorem deriv_pow' {𝕜 : Type u} (n : ) :
deriv (λ (x : 𝕜), x ^ n) = λ (x : 𝕜), n * x ^ (n - 1)
theorem deriv_within_pow {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (n : ) (hxs : x) :
deriv_within (λ (x : 𝕜), x ^ n) s x = n * x ^ (n - 1)
theorem has_deriv_within_at.pow {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {c : 𝕜 𝕜} {c' : 𝕜} (n : ) (hc : s x) :
has_deriv_within_at (λ (y : 𝕜), c y ^ n) (n * c x ^ (n - 1) * c') s x
theorem has_deriv_at.pow {𝕜 : Type u} {x : 𝕜} {c : 𝕜 𝕜} {c' : 𝕜} (n : ) (hc : c' x) :
has_deriv_at (λ (y : 𝕜), c y ^ n) (n * c x ^ (n - 1) * c') x
theorem deriv_within_pow' {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {c : 𝕜 𝕜} (n : ) (hc : x) (hxs : x) :
deriv_within (λ (x : 𝕜), c x ^ n) s x = n * c x ^ (n - 1) * s x
@[simp]
theorem deriv_pow'' {𝕜 : Type u} {x : 𝕜} {c : 𝕜 𝕜} (n : ) (hc : x) :
deriv (λ (x : 𝕜), c x ^ n) x = n * c x ^ (n - 1) * x