Commit 2025-01-17 10:17 e5ab45ea

feat: definition of linear topologies (#14990) A topology on a module is linear if it is invariant by translation and if there is a basis of neighborhoods consisting of submodules. We are most interested in the case of rings: a topology on a ring is linear if it is linear for both the left- and right-module structures on R over itself. This is equivalent to being invariant by translation and admitting a basis of neighborhoods consisting of two-sided ideals. This will be used in a subsequent PR to evaluate multivariate power series. We will also show that the natural topology on MvPowerSeries S R is a linear topology when S has a linear topology (e.g the discrete topology).