Commit 2024-07-20 15:54 5e0c71f3

View on Github →

feat(RingTheory/Powerseries): generalize coeff_one_pow (#14895) Removes the condition of coeff_one_pow that the constant coefficient must be 1.

Estimated changes

modified theorem PowerSeries.coeff_one_pow