pow — Mathlib

English

If f has a strict derivative at x, then for every n, the strict derivative of f^n at x is given by the same summation formula.

Русский

Если у f есть строгое производное в x, то для каждого n строгая производная f(x)^n в x равна той же сумме.

LaTeX

$$$$\text{HasStrictDerivAt}(f^n,\; n\cdot f(x)^{n-1}\cdot f',\; x) = \cdots $$$$

Lean4

nonrec theorem pow (h : HasStrictDerivAt f f' x) (n : ℕ) : HasStrictDerivAt (f ^ n) (n * f x ^ (n - 1) * f') x :=
  h.fun_pow n

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