sum_antidiagonal_choose_add — Mathlib

English

For natural numbers d and n, the sum over the antidiagonal n of (d + j) choose d equals (d + n + 1) choose (d + 1).

Русский

Для натуральных чисел d и n сумма по антидиагонали n от (d + j) выбрать d равна (d + n + 1) выбрать (d + 1).

LaTeX

$$$$\sum_{(i,j) \in \operatorname{antidiagonal}(n)} \binom{d + j}{d} = \binom{d + n + 1}{d + 1}.$$$$

Lean4

theorem sum_antidiagonal_choose_add (d n : ℕ) :
    (∑ ij ∈ antidiagonal n, (d + ij.2).choose d) = (d + n + 1).choose (d + 1) := by
  induction n with
  | zero => simp
  | succ n hn => rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]

Похожие утверждения