English
Hockey-stick identity: the sum of binomial coefficients along the diagonal Icc equals a shifted binomial coefficient: ∑_{m=0}^n C(m,k) = C(n+1,k+1).
Русский
Идентичность хоккейной палки: сумма коэффициентов бинома вдоль диагонали Icc равна смещённому биномиальному коэффициенту: ∑_{m=0}^n C(m,k) = C(n+1,k+1).
LaTeX
$$$\sum_{m=\,k}^{n} {m\choose k} = {n+1 \choose k+1}$$$
Lean4
/-- **Zhu Shijie's identity** aka hockey-stick identity, version with `Icc`. -/
theorem sum_Icc_choose (n k : ℕ) : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1) :=
by
rcases lt_or_ge n k with h | h
· rw [choose_eq_zero_of_lt (by cutsat), Icc_eq_empty_of_lt h, sum_empty]
·
induction n, h using le_induction with
| base => simp
| succ n _ ih =>
rw [← Ico_insert_right (by cutsat), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih, choose_succ_succ' (n + 1)]
