Theorem PowerSeries.WithPiTopology.tendsto_trunc_atTop

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