Theorem MvPowerSeries.LinearTopology.basis_le_iff

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