Theorem PowerSeries.derivativeFun_add

Modification history

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