Theorem MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeries

Modification history

2025-05-21 12:33
Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
chore(RingTheory/MvPowerSeries/PiTopology): limit of truncation of power series (#23643) …
Added MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeriesView on Github →