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 .

source

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