deriv_pow'' — Mathlib

English

For 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_pow (since := "2025-07-16")]
theorem deriv_pow'' {c : 𝕜 → 𝕜} (n : ℕ) (hc : DifferentiableAt 𝕜 c x) :
    deriv (c ^ n) x = (n : 𝕜) * c x ^ (n - 1) * deriv c x :=
  deriv_pow hc n

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