Theorem MvPowerSeries.LinearTopology.basis_le

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_leView on Github →