sumIDeriv_apply — Mathlib

English

For any polynomial p, sumIDeriv p equals the finite sum over i of derivative^i p, i.e., the i-th iterate of derivative summed over i in range.

Русский

Для любого полинома p, sumIDeriv p равен конечной сумме по i от производной в i-й степени, т.е. сумме итераций производной по i.

LaTeX

$$$\forall p:R[X],\ sumIDeriv\ p = \sum_{i\in range\ (p.natDegree+1)} (derivative)^{i} p$$$

Lean4

theorem sumIDeriv_apply (p : R[X]) : sumIDeriv p = ∑ i ∈ range (p.natDegree + 1), derivative^[i] p :=
  by
  dsimp [sumIDeriv]
  exact Finsupp.sum_of_support_subset _ (by simp) _ (by simp)

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