deriv_rpow_const — Mathlib

English

If f is differentiable at x with derivative f', and f(x) ≠ 0 or p ≥ 1, then the derivative at x of f(x)^p is f'(x) p f(x)^{p−1}. More precisely, deriv (f^p)(x) = deriv f(x) · p · f(x)^{p−1}.

Русский

Если f дифференцируема в точке x и f(x) ≠ 0 или p ≥ 1, то производная в точке x функции f(x)^p равна f'(x) p f(x)^{p−1}. Точнее: d/dx [f(x)^p] = f'(x) p f(x)^{p−1}.

LaTeX

$$$\\displaystyle \\frac{d}{dx}\\bigl(f(x)^p\\bigr) = f'(x) \\cdot p \\cdot f(x)^{\\,p-1}$$$

Lean4

@[simp]
theorem deriv_rpow_const (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0 ∨ 1 ≤ p) :
    deriv (fun x => f x ^ p) x = deriv f x * p * f x ^ (p - 1) :=
  (hf.hasDerivAt.rpow_const hx).deriv

Похожие утверждения