Theorems · Theorem · difference equations

fwdDiff_iter_sum_mul_pow_eq_zero

∀ {R : Type u_3} [inst : CommRing R] {n : ℕ} (P : ℕ → R),
  ((fwdDiff 1)^[n] fun r => ∑ k ∈ Finset.range n, P k * r ^ k) = 0

The n-th forward difference of a polynomial of degree < n is zero (formulated using explicit sums over range n).

Defined in

Mathlib.Algebra.Group.ForwardDiff

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing