Commit 2025-02-17 18:49 447722b3

feat(RingTheory.MvPowerSeries.LinearTopology): a linear topology on the ring of power series (#15007)

• MvPowerSeries.basis: the ideals of the ring of multivariate power series all coefficients the exponent of which is smaller than some bound vanish.
• MvPowerSeries.isLinearTopology : if R has a linear topology, then the product topology on MvPowerSeries σ R is a linear topology, as witnessed by the ideals from MvPowerSeries.basis which form a basis of neighborhoods of 0 consisting of two-sided ideals. This applies in particular when R has the discrete topology.