Theorem MvPowerSeries.order_expand

Modification history

2026-01-18 13:18

Mathlib/RingTheory/MvPowerSeries/Expand.lean

feat(RingTheory/MvPowerSeries): some theorems about expand (#33885)

Added MvPowerSeries.order_expand View on Github →