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_deriv_within_at_pow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(n : ℕ)
(x : 𝕜)
(s : set 𝕜) :
theorem
differentiable_at_pow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
(n : ℕ) :
differentiable_at 𝕜 (λ (x : 𝕜), x ^ n) x
theorem
differentiable_within_at_pow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(n : ℕ) :
differentiable_within_at 𝕜 (λ (x : 𝕜), x ^ n) s x
theorem
differentiable_pow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(n : ℕ) :
differentiable 𝕜 (λ (x : 𝕜), x ^ n)
theorem
differentiable_on_pow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{s : set 𝕜}
(n : ℕ) :
differentiable_on 𝕜 (λ (x : 𝕜), x ^ n) s
theorem
deriv_within_pow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(n : ℕ)
(hxs : unique_diff_within_at 𝕜 s x) :
theorem
has_deriv_within_at.pow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{c : 𝕜 → 𝕜}
{c' : 𝕜}
(n : ℕ)
(hc : has_deriv_within_at c c' s x) :
theorem
has_deriv_at.pow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{c : 𝕜 → 𝕜}
{c' : 𝕜}
(n : ℕ)
(hc : has_deriv_at c c' x) :
theorem
deriv_within_pow'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{c : 𝕜 → 𝕜}
(n : ℕ)
(hc : differentiable_within_at 𝕜 c s x)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (x : 𝕜), c x ^ n) s x = ↑n * c x ^ (n - 1) * deriv_within c s x