deriv_pow' — Mathlib

English

If f is differentiable at x with derivative f', then for every n, the derivative of f^n at x is ∑_{i=0}^{n-1} f(x)^{n-1-i} f'(x) f(x)^i.

Русский

Если f дифференцируема в x с производной f'(x), то для любого n производная f(x)^n в x равна сумме ∑_{i=0}^{n-1} f(x)^{n-1-i} f'(x) f(x)^i.

LaTeX

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

Lean4

@[simp low]
theorem deriv_pow' (h : DifferentiableAt 𝕜 f x) (n : ℕ) :
    deriv (f ^ n) x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * deriv f x * f x ^ i :=
  deriv_fun_pow' h n

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