pow — Mathlib

English

If f is strictly differentiable at x, then f^n has derivative (n f(x)^{n-1}) f'(·) in the appropriate sense.

Русский

Если f имеет строгую производную в точке x, то производная f^n составляет (n f(x)^{n-1}) умножение на производную f.

LaTeX

$$$\\text{HasStrictFDerivAt}_{\\mathbb{K}}(f^n)(x) = (n\\,f(x)^{n-1})\\cdot f'(x) \\\\ (n\\in\\mathbb{N}).$$$

Lean4

theorem pow (h : HasStrictFDerivAt f f' x) (n : ℕ) : HasStrictFDerivAt (fun x ↦ f x ^ n) ((n • f x ^ (n - 1)) • f') x :=
  h.pow' n |>.congr_fderiv <| aux_sum_eq_pow _

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