### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Falling_Factorial_Sum

- Falling_Factorial_Sum_Combinatorics
- Falling_Factorial_Sum_Induction
- Falling_Factorial_Sum_Vandermonde

### Depends on

- Cardinality of Set Partitions
- Discrete Summation

### Used by

- Combinatorial Enumeration Algorithms

## Cite

×

Falling_Factorial_Sum-AFP

    @article{Falling_Factorial_Sum-AFP,
      author  = {Lukas Bulwahn},
      title   = {The Falling Factorial of a Sum},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Falling_Factorial_Sum.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Dec 30, 2017 : Isabelle2017