Theorem Finset.sum_antidiagonal_choose_add

Modification history

2024-05-16 20:36

Mathlib/Data/Nat/Choose/Sum.lean

feat(RingTheory/PowerSeries/WellKnown): the power series of `1 / ((1 - x) ^ (d + 1))` with coefficients in a commutative ring `S`, where `d : ℕ`. (#11255)

Added Finset.sum_antidiagonal_choose_add View on Github →