English
Let f: 𝕂 → 𝔸 be differentiable at x within a set s with derivative f'. Then for every n ≥ 0, the derivative of x ↦ f(x)^n at x (within s) is given by the finite sum ∑_{i=0}^{n-1} f(x)^{n-1-i} f' f(x)^i.
Русский
Пусть f: 𝕂 → 𝔸 дифференцируема в точке x на множестве s, и ее производная равна f'. Тогда для каждого натурального n ≥ 0 производная функции x ↦ f(x)^n в точке x (на s) равна сумме ∑_{i=0}^{n-1} f(x)^{n-1-i} f' 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
nonrec theorem fun_pow' (h : HasDerivWithinAt f f' s x) (n : ℕ) :
HasDerivWithinAt (fun x ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x := by
simpa using h.hasFDerivWithinAt.pow' n |>.hasDerivWithinAt
