pow' — Mathlib

English

Let h be a derivative within s of f at x with value f'. Then for every n, the derivative of f^n is the same sum formula as above with f' in the middle.

Русский

Пусть h является производной внутри s от f в x со значением f'. Тогда для каждого n производная f(x)^n равна той же сумме с f' посередине.

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

nonrec theorem pow' (h : HasDerivWithinAt f f' s x) (n : ℕ) :
    HasDerivWithinAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x :=
  h.fun_pow' n

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