sumIDeriv_apply_of_le — Mathlib

English

If natDegree(p) ≤ n, then sumIDeriv p equals the sum over i from 0 to n of derivative^i p.

Русский

Если natDegree(p) ≤ n, то sumIDeriv p равен сумме производных в степенях 0..n.

LaTeX

$$$p.natDegree \le n \Rightarrow sumIDeriv p = \sum_{i=0}^{n} (derivative)^{i} p$$$

Lean4

theorem sumIDeriv_apply_of_le {p : R[X]} {n : ℕ} (hn : p.natDegree ≤ n) :
    sumIDeriv p = ∑ i ∈ range (n + 1), derivative^[i] p :=
  by
  dsimp [sumIDeriv]
  exact Finsupp.sum_of_support_subset _ (by simp [Nat.lt_succ, hn]) _ (by simp)

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