Theorem PowerSeries.coeff_one_pow

Modification history

2024-07-20 15:54
Mathlib/RingTheory/PowerSeries/Basic.lean
feat(RingTheory/Powerseries): generalize `coeff_one_pow` (#14895) …
Modified PowerSeries.coeff_one_powView on Github →
2024-07-14 07:35
Mathlib/RingTheory/PowerSeries/Basic.lean
feat(PowerSeries): coefficients of series products (#14452) …
Added PowerSeries.coeff_one_powView on Github →