Theorem MvPowerSeries.map_expand

Modification history

2025-12-18 09:08

Mathlib/RingTheory/MvPowerSeries/Expand.lean

feat(RingTheory/MvPowerSeries): some APIs about `expand` (#33005) …

Added MvPowerSeries.map_expand View on Github →