Theorem PowerSeries.derivativeFun_one

Modification history

2023-10-26 11:12

Mathlib/RingTheory/PowerSeries/Derivative.lean

feat (RingTheory/PowerSeries) add formal derivative operation (#7820) …

Added PowerSeries.derivativeFun_one View on Github →