English
A Chu-Vandermonde identity for binomial rings: choose (r+s) k equals the sum over antidiagonal of choose r i times choose s k−i.
Русский
Идентичность Чу-Вандермонде для биномиальных колец: choose (r+s) k = сумма по антидиагонали выбираемых пар (i, k−i) множителей choose r i и choose s (k−i).
LaTeX
$$$ \forall R\ [Ring\ R]\ [BinomialRing\ R]\ {r s: R} (k: \mathbb{N}) (h: Commute r s),\ \text{choose} (r+s) k = \sum_{ij \in antidiagonal k} \text{choose} r ij.1 \cdot \text{choose} s ij.2$$$
Lean4
/-- The Chu-Vandermonde identity for binomial rings -/
theorem add_choose_eq [Ring R] [BinomialRing R] {r s : R} (k : ℕ) (h : Commute r s) :
choose (r + s) k = ∑ ij ∈ antidiagonal k, choose r ij.1 * choose s ij.2 :=
by
rw [← nsmul_right_inj (Nat.factorial_ne_zero k), ← descPochhammer_eq_factorial_smul_choose, smul_sum,
descPochhammer_smeval_add _ h]
refine sum_congr rfl ?_
intro x hx
rw [← Nat.choose_mul_factorial_mul_factorial (antidiagonal.fst_le hx),
tsub_eq_of_eq_add_rev (List.Nat.mem_antidiagonal.mp hx).symm, mul_assoc, nsmul_eq_mul, Nat.cast_mul, Nat.cast_mul, ←
mul_assoc _ (x.1.factorial : R), mul_assoc _ (x.2.factorial : R), ← mul_assoc (x.2.factorial : R),
Nat.cast_commute x.2.factorial, mul_assoc _ (x.2.factorial : R), ← nsmul_eq_mul x.2.factorial]
simp [mul_assoc, descPochhammer_eq_factorial_smul_choose]
