deriv_fun_pow'' — Mathlib

English

For a general c: 𝕜 → 𝕜, differentiable at x, the derivative of c(x)^n is n c(x)^{n-1} c'(x).

Русский

Для произвольной c: 𝕜→𝕜, дифференцируемой в x, производная c(x)^n равна n c(x)^{n-1} c'(x).

LaTeX

$$$$\\frac{d}{dx}\\bigl(c(x)^n\\bigr)=n\\,c(x)^{\,n-1}\\,c'(x). $$$$

Lean4

@[deprecated deriv_fun_pow (since := "2025-07-16")]
theorem deriv_fun_pow'' {c : 𝕜 → 𝕜} (n : ℕ) (hc : DifferentiableAt 𝕜 c x) :
    deriv (fun x => c x ^ n) x = (n : 𝕜) * c x ^ (n - 1) * deriv c x :=
  deriv_fun_pow hc n

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