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

Commits

Commits on May 20, 2026

Commits on Jun 26, 2026

Commits on Jun 27, 2026

Commits on Jul 15, 2026

Commits on Jul 16, 2026