Commit 2026-09-07 14:31 3c2928f1

View on Github →

chore(MvPowerSeries/Derivative): make coeff ring implicit (#43334) In this PR, we make the coeff ring R in the definition of derivative implicit.

Estimated changes

modified theorem MvPowerSeries.pderiv_C
modified theorem MvPowerSeries.pderiv_X_self
modified theorem MvPowerSeries.pderiv_one
modified theorem PowerSeries.derivative.ext
modified theorem PowerSeries.derivative_C
modified theorem PowerSeries.derivative_X
modified theorem PowerSeries.derivative_coe
modified theorem PowerSeries.derivative_inv'
modified theorem PowerSeries.derivative_one
modified theorem PowerSeries.derivative_log