pow' — Mathlib

English

Under the HasStrictDerivAt framework, the derivative of f^n at x is the sum over i of f(x)^{n-1-i} f' f(x)^i for i=0,...,n-1.

Русский

В рамках HasStrictDerivAt производная f^n в x равна сумме по i от f(x)^{n-1-i} f' f(x)^i, i=0,...,n-1.

LaTeX

$$$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

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

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