fderivWithin_pow_ring' — Mathlib

English

Same derivative formula for f^n applies, stated with fderiv.

Русский

Та же формула производной для f^n выражена через fderiv.

LaTeX

$$$fderiv( f^n)(x) = \\sum_{i=0}^{n-1} f(x)^{n-1-i} \\; fderiv(f)(x) \\; f(x)^i.$$$

Lean4

theorem fderivWithin_pow_ring' {s : Set 𝔸} {x : 𝔸} (n : ℕ) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun x : 𝔸 ↦ x ^ n) s x = (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> .id _ _ <• x ^ i) := by
  rw [fderivWithin_fun_pow' hxs n differentiableAt_fun_id.differentiableWithinAt, fderivWithin_id' hxs]

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