pow — Mathlib

English

If f is differentiable at x with derivative f', then for every n, HasDerivAt 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

theorem pow (h : HasDerivAt f f' x) (n : ℕ) : HasDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x :=
  h.fun_pow n

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