Vandermonde's identity

Stream: Is there code for X?

[Johan Commelin]

Do we have https://en.wikipedia.org/wiki/Vandermonde%27s_identity ?

import data.finset.nat_antidiagonal

open_locale big_operators

lemma nat.add_choose_eq (m n k : ℕ) :
  (m + n).choose k = ∑ (ij : ℕ × ℕ) in finset.nat.antidiagonal k, m.choose ij.1 * n.choose ij.2 :=
sorry

[Yaël Dillies]

Pretty sure we don't. Would be a great sumaddition!

[Johan Commelin]

-- move this
section
open polynomial finset.nat

lemma polynomial.X_add_one_pow_coeff (R : Type*) [semiring R] (n k : ℕ) :
  ((X + 1) ^ n).coeff k = (n.choose k : R) :=
begin
  rw [(commute_X (1 : polynomial R)).add_pow, ← lcoeff_apply, linear_map.map_sum],
  simp only [one_pow, mul_one, lcoeff_apply, ← C_eq_nat_cast, coeff_mul_C, nat.cast_id],
  rw [finset.sum_eq_single k, coeff_X_pow_self, one_mul],
  { intros _ _,
    simp only [coeff_X_pow, boole_mul, ite_eq_right_iff, ne.def] {contextual := tt},
    rintro h rfl, contradiction },
  { simp only [coeff_X_pow_self, one_mul, not_lt, finset.mem_range],
    intro h, rw [nat.choose_eq_zero_of_lt h, nat.cast_zero], }
end

open polynomial

/-- Vandermonde's identity -/
lemma nat.add_choose_eq (m n k : ℕ) :
  (m + n).choose k = ∑ (ij : ℕ × ℕ) in antidiagonal k, m.choose ij.1 * n.choose ij.2 :=
begin
  calc (m + n).choose k
      = ((X + 1) ^ (m + n)).coeff k : _
  ... = ((X + 1) ^ m * (X + 1) ^ n).coeff k : by rw pow_add
  ... = ∑ (ij : ℕ × ℕ) in antidiagonal k, m.choose ij.1 * n.choose ij.2 : _,
  { rw [X_add_one_pow_coeff, nat.cast_id], },
  { rw [coeff_mul, finset.sum_congr rfl],
    simp only [X_add_one_pow_coeff, nat.cast_id, eq_self_iff_true, imp_true_iff], }
end

end

[Kevin Buzzard]

That's an innovative proof!

[Johan Commelin]

It's on wiki

[Johan Commelin]

It's a bit high-powered maybe. But being able to use coeff_mul is very pleasant.

[Eric Wieser]

Shouldn't that be called coeff_X_add_one_pow? I'm quite surprised we don't have that lemma, which makes me think maybe we do but it's named differently or the + is backwards

[Johan Commelin]

rg "coeff.*choose" doesn't give me any hits in mathlib.

[Johan Commelin]

#8992