fderivWithin_pow_ring — Mathlib

English

Within a set, the derivative of the power map on a ring is the same sum with within-derivative terms.

Русский

Внутри множества производная x^n на кольце — та же сумма с внутренними членами.

LaTeX

$$$fderivWithin_{\\mathbb{K}}(x\\mapsto x^n)(s,x) = \\sum_{i=0}^{n-1} x^{n-1-i} \\; fderivWithin_{\\mathbb{K}}id(s,x) \\; x^i.$$$

Lean4

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

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