Theorem PowerSeries.derivative_coe

Modification history

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