The Falling Factorial of a Sum

Lukas Bulwahn 📧

December 22, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry shows that the falling factorial of a sum can be computed with an expression using binomial coefficients and the falling factorial of its summands. The entry provides three different proofs: a combinatorial proof, an induction proof and an algebraic proof using the Vandermonde identity. The three formalizations try to follow their informal presentations from a Mathematics Stack Exchange page as close as possible. The induction and algebraic formalization end up to be very close to their informal presentation, whereas the combinatorial proof first requires the introduction of list interleavings, and significant more detail than its informal presentation.


BSD License


Session Falling_Factorial_Sum