fderiv_pow_ring' — Mathlib

English

In a (nontrivial) ring, the derivative of x ↦ x^n at x is the sum of left-right multiplications: ∑_{i=0}^{n-1} x^{n-1-i} h x^{i} for increment h.

Русский

В кольце производная функции x ↦ x^n в точке x есть сумма слева и справа: ∑ 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 fderiv_pow_ring' {x : 𝔸} (n : ℕ) :
    fderiv 𝕜 (fun x : 𝔸 ↦ x ^ n) x = (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> .id _ _ <• x ^ i) := by
  rw [fderiv_fun_pow' n differentiableAt_fun_id, fderiv_id']

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