mathlib documentation

data.nat.choose.vandermonde

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 : ) :
(m + n).choose k = ∑ (ij : × ) in finset.nat.antidiagonal k, (m.choose ij.fst) * n.choose ij.snd

Vandermonde's identity