pow' — Mathlib

English

The HasFDerivAt.pow' rule asserts the same power-derivative formula in HasFDerivAt form, i.e., the derivative of f^n is the same finite sum with left and right scalar actions.

Русский

Правило HasFDerivAt.pow' формулирует ту же формулу производной степени в форме HasFDerivAt.

LaTeX

$$$\\text{HasFDerivAt}\\ f f' x \\Rightarrow \\text{HasFDerivAt}\\ (f^n)\\ (\\sum_{i})\\ x$$$

Lean4

theorem pow' (h : HasFDerivAt f f' x) (n : ℕ) :
    HasFDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x :=
  h.fun_pow' n

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