Theorem MvPowerSeries.WithPiTopology.tendsto_trunc_atTop

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.tendsto_trunc_atTopView on Github →