Commit 2024-12-02 11:59 7b33f44e

feat(RingTheory.MvPowerSeries.Topology): define the product topology on mv power series (#14866) Let R be with Semiring R and TopologicalSpace R In this file we define the topology on MvPowerSeries σ R that corresponds to the simple convergence on its coefficients, aka the product topology. It is the coarsest topology for which all coefficients maps are continuous. When R has UniformSpace R, we define the corresponding uniform structure. When the type of coefficients has the discrete topology, it corresponds to the topology defined by [bourbaki1981], chapter 4, §4, n°2 Coauthored with María Inés de Frutos Fernández @mariainesdff