English
If f has a strict derivative f' at x, then for every n ∈ ℕ, the function x ↦ f(x)^n has derivative equal to the sum from i=0 to n-1 of f(x)^{n-1-i} f' f(x)^i at x. This is the standard power rule for a function with a derivative.
Русский
Если f имеет строгую производную f' в точке x, то для каждого n ∈ ℕ производная функции x ↦ f(x)^n равна сумме по i=0..n-1 от f(x)^{n-1-i} f' f(x)^i в точке x; это обычное правило степени.
LaTeX
$$$\text{HasStrictDerivAt}\left( f, f', x \right) \Rightarrow \forall n,\ HasStrictDerivAt\left( f^n, \sum_{i=0}^{n-1} f(x)^{n-1-i} \cdot f' \cdot f(x)^i, x \right)$$$
Lean4
protected theorem fderivWithin_aeval (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun x => aeval x q) s x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (aeval x (derivative q)) :=
(q.hasFDerivWithinAt_aeval x).fderivWithin hxs
