mathlib3 documentation

data.nat.choose.vandermonde

Vandermonde's identity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Vandermonde's identity