Theorem PowerSeries.WithPiTopology.denseRange_toPowerSeries

Modification history

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