pow' — Mathlib

English

For HasDerivAt, if f has derivative f' at x, then the derivative of f^n at x is the same sum with f(x) and f'(x).

Русский

Для HasDerivAt, если у f в точке x производная f', то производная f(x)^n в x равна той же сумме с f(x) и f'(x).

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) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x :=
  h.fun_pow' n

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