Sums of binomial coefficients #
This file includes variants of the binomial theorem and other results on sums of binomial coefficients. Theorems whose proofs depend on such sums may also go in this file for import reasons.
A version of
Commute.add_pow that avoids ℕ-subtraction by summing over the antidiagonal and
also with the binomial coefficient applied via scalar action of ℕ.
The sum of
(n+1).choose i * f i (n+1-i) can be split into two sums at rank
n.choose i * f i (n+1-i) and
n.choose i * f (i+1) (n-i).
The sum along the antidiagonal of
(n+1).choose i * f i j can be split into two sums along the
antidiagonal at rank
n, respectively of
n.choose i * f i (j+1) and
n.choose j * f (i+1) j.