Alternating binomial convolution coefficient over a commutative ring

Proved

Nat.alternating_choose_convolution

by Mazecto · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebracombinatorics

For any commutative ring R and natural numbers n,m,

\sum_{k=0}^{n}\binom{n}{k}(-1)^k\binom{k}{m}=\begin{cases}(-1)^n,&m=n,\\0,&m\ne n.\end{cases}

The identity includes m>n, n=0 and rings of positive characteristic. It is the coefficient cancellation underlying finite binomial inversion.

Preamble

import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Tactic.LinearCombination

open Finset

Formal statement

theorem Nat.alternating_choose_convolution {R : Type*} [CommRing R] (n m : ℕ) :
    (∑ k ∈ range (n + 1), (n.choose k : R) * (-1 : R)^k * (k.choose m : R)) =
      if m = n then (-1 : R)^n else 0 := by sorry

Source

Derived coefficient identity from Nat.choose_mul and Int.alternating_sum_range_choose in pinned Mathlib 0df444a360eaa60ab8c11dca51a86af692955474, Mathlib/Data/Nat/Choose/Basic.lean and Sum.lean: https://github.com/leanprover-community/mathlib4/tree/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Data/Nat/Choose. This commutative-ring coefficient formulation is a derived lemma, rather than a quoted source theorem.

View graph