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 ℕ.