Commit 2024-10-17 17:56 9d883e28
View on Github →feat(RingTheory/PowerSeries/WellKnown): changed PowerSeries.invOneSubPow (#17360)
The definition of PowerSeries.invOneSubPow has been changed into the following:
Given a commutative ring S and a number d : ℕ, PowerSeries.invOneSubPow S d is the multiplicative inverse of (1 - X) ^ d in S⟦X⟧ˣ. When d is 0, PowerSeries.invOneSubPow S d will just be 1. When d is positive, PowerSeries.invOneSubPow S d will be ∑ n, Nat.choose (d - 1 + n) (d - 1).