Vandermonde's identity #
In this file we prove Vandermonde's identity (Nat.add_choose_eq):
(m + n).choose k = ∑ (ij : ℕ × ℕ) in antidiagonal k, m.choose ij.1 * n.choose ij.2
We follow the algebraic proof from https://en.wikipedia.org/wiki/Vandermonde%27s_identity#Algebraic_proof .
theorem
Nat.add_choose_eq
(m : ℕ)
(n : ℕ)
(k : ℕ)
:
Nat.choose (m + n) k = Finset.sum (Finset.antidiagonal k) fun (ij : ℕ × ℕ) => Nat.choose m ij.1 * Nat.choose n ij.2
Vandermonde's identity