English
For natural numbers m, n, k, the binomial coefficient (m+n choose k) equals the sum over all pairs i,j with i+j=k of m choose i times n choose j.
Русский
Для натуральных m, n, k тождество Вандермонде: (m+n) выбрать k равно сумме по всем парам i,j с i+j=k из m выбрать i умножить на n выбрать j.
LaTeX
$$$$\binom{m+n}{k} = \sum_{i+j=k} \binom{m}{i} \binom{n}{j} = \sum_{i=0}^{k} \binom{m}{i} \binom{n}{k-i}.$$$$
Lean4
/-- Vandermonde's identity -/
theorem add_choose_eq (m n k : ℕ) : (m + n).choose k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
calc
(m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, Nat.cast_id]
_ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
_ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 :=
by
rw [coeff_mul, Finset.sum_congr rfl]
simp only [coeff_X_add_one_pow, Nat.cast_id, imp_true_iff]
