fderivWithin_pow — Mathlib

English

For the map x ↦ x^n on a ring, the derivative is the sum of left-right multiplications: ∑ x^{n-1-i} · h · x^i.

Русский

Для отображения x ↦ x^n на кольце производная есть сумма слева и справа: ∑ x^{n-1-i} h x^i.

LaTeX

$$$D_x(x\\mapsto x^n)(h) = \\sum_{i=0}^{n-1} x^{\\,n-1-i} h x^{i}.$$$

Lean4

theorem fderivWithin_pow (hxs : UniqueDiffWithinAt 𝕜 s x) (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) :
    fderivWithin 𝕜 (f ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x :=
  fderivWithin_fun_pow hxs n hf

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