Def MvPowerSeries.LinearTopology.basis

Modification history

2026-02-24 10:38
Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
chore: bump toolchain to v4.29.0-rc2 (#35708)
Deleted MvPowerSeries.LinearTopology.basisView on Github →
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.basisView on Github →