Theorem MvPowerSeries.LinearTopology.hasBasis_nhds_zero

Modification history

2025-02-17 18:49
Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
feat(RingTheory.MvPowerSeries.LinearTopology): a linear topology on the ring of power series (#15007) …
Added MvPowerSeries.LinearTopology.hasBasis_nhds_zeroView on Github →