Theorem MvPowerSeries.LinearTopology.mem_basis_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.mem_basis_iffView on Github →