Forward_Difference_of_Falling_Factorial
Provedcombinatoricsfinite-differencesproofwiki
The forward difference of the falling factorial x^(n) is n * x^(n-1).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Forward_Difference_of_Falling_Factorial (n : ℕ) (x : ℝ) : (x + 1) * (Finset.range n).prod (fun i => (x - (i : ℝ))) - (Finset.range (n + 1)).prod (fun i => (x - (i : ℝ))) = ((n : ℝ) + 1) * (Finset.range n).prod (fun i => (x - (i : ℝ))) := by sorry
Source