Skip to content

[Merged by Bors] - feat(RingTheory/MvPowerSeries): partial derivatives of MvPowerSeries#39626

Closed
justus-springer wants to merge 12 commits into
leanprover-community:masterfrom
justus-springer:justus/MvPowerSeries_pderiv
Closed

[Merged by Bors] - feat(RingTheory/MvPowerSeries): partial derivatives of MvPowerSeries#39626
justus-springer wants to merge 12 commits into
leanprover-community:masterfrom
justus-springer:justus/MvPowerSeries_pderiv