lean_workbook_plus_34585

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove the identity $\sum_{k=0}^m(-1)^k\binom{2n+1}{k}=(-1)^m\binom{2n}{m}$ using induction over $m$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34585 (n m : ℕ) : ∑ k in Finset.range (m+1), (-1 : ℤ)^k * (2*n+1).choose k = (-1)^m * (2*n).choose m   :=  by sorry

Source