Theorem PowerSeries.coeff_derivativeFun

Modification history

2023-10-26 11:12
Mathlib/RingTheory/PowerSeries/Derivative.lean
feat (RingTheory/PowerSeries) add formal derivative operation (#7820) …
Added PowerSeries.coeff_derivativeFunView on Github →