Commit 2023-10-26 11:12 d8e5144d

View on Github →

feat (RingTheory/PowerSeries) add formal derivative operation (#7820) Given a commutative semiring R, define the formal derivative R[[X]] \to R[[X]] and prove some basic properties. This is a part of #7271.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/PowerSeries/Derivative.lean

added theorem PowerSeries.coeff_derivative

added theorem PowerSeries.coeff_derivativeFun

added theorem PowerSeries.derivative.ext

added theorem PowerSeries.derivativeFun_C

added theorem PowerSeries.derivativeFun_add

added theorem PowerSeries.derivativeFun_coe

added theorem PowerSeries.derivativeFun_mul

added theorem PowerSeries.derivativeFun_one

added theorem PowerSeries.derivativeFun_smul

added theorem PowerSeries.derivative_C

added theorem PowerSeries.derivative_X

added theorem PowerSeries.derivative_coe

added theorem PowerSeries.derivative_inv'

added theorem PowerSeries.derivative_inv

added theorem PowerSeries.derivative_invOf

added theorem PowerSeries.trunc_derivative'

added theorem PowerSeries.trunc_derivative

added theorem PowerSeries.trunc_derivativeFun