Commit 2026-07-16 12:42 044efe50

feat(RingTheory/MvPowerSeries): partial derivatives of MvPowerSeries (#39626) Previously, we had formal derivatives for PowerSeries and Polynomial and formal partial derivatives for MvPolynomial, but no formal partial derivatives for MvPowerSeries. This PR adds them. Furthermore, PowerSeries.derivative is refactored to be defined in terms of MvPowerSeries.pderiv, which reduces code duplication (In particular, there is no need to define the bare function PowerSeries.derivativeFun anymore). Most proofs are direct generalizations from the univariate case. I only had to add a few missing API lemmas, which I am PR'ing separately below:

• depends on: #39623
• depends on: #39624
• depends on: #39625