alternating_sum_range_choose — Mathlib

English

An alternating sum of binomial coefficients over a finite range yields a simple closed form depending on parity.

Русский

Чередующая сумма биномиальных коэффициентов по диапазону даёт простую форму закрытой записи в зависимости от паритета.

LaTeX

$$$\sum_{m=0}^n (-1)^m {n\choose m} = (1-1)^n = 0$ for n>0 and equals 1 for n=0$$

Lean4

theorem alternating_sum_range_choose {n : ℕ} :
    (∑ m ∈ range (n + 1), ((-1) ^ m * n.choose m : ℤ)) = if n = 0 then 1 else 0 := by
  cases n with
  | zero => simp
  | succ n =>
    have h := add_pow (-1 : ℤ) 1 n.succ
    simp only [one_pow, mul_one, neg_add_cancel] at h
    rw [← h, zero_pow n.succ_ne_zero, if_neg n.succ_ne_zero]

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