hasStrictFDerivAt_pow — Mathlib

English

For the map x ↦ x^n on a ring, the derivative at x is the linear map h ↦ ∑_{i=0}^{n-1} x^{n-1-i} h x^i.

Русский

Для отображения x ↦ x^n на кольце производная в точке x есть линейный оператор h ↦ ∑ 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 hasStrictFDerivAt_pow (n : ℕ) {x : 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x : 𝔸 ↦ x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) x :=
  hasStrictFDerivAt_id _ |>.pow n

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