fderiv_pow_ring — Mathlib

English

In a ring, the derivative of x^n at x is the sum ∑ x^{n-1-i} h x^i for increment h.

Русский

В кольце производная x^n в точке x равна сумме ∑ x^{n-1-i} h x^i для приращения h.

LaTeX

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

Lean4

theorem fderiv_pow_ring {x : 𝔸} (n : ℕ) : fderiv 𝕜 (fun x : 𝔸 ↦ x ^ n) x = (n • x ^ (n - 1)) • .id _ _ := by
  rw [fderiv_fun_pow n differentiableAt_fun_id, fderiv_id']

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