2024-05-16 20:36
Mathlib/RingTheory/PowerSeries/WellKnown.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 PowerSeries.mk_one_pow_eq_mk_choose_add