mathlib3

10721bab - feat(topology/algebra/module/basic): basic topological properties of quotient modules (#13433)

feat(topology/algebra/module/basic): basic topological properties of quotient modules (#13433) More precisely, we prove that : * if `M` is a topological module and `S` is a submodule of `M`, then `M ⧸ S` is a topological module * furthermore, if `S` is closed, then `M ⧸ S` is regular (hence T2) - [x] depends on: #13278 - [x] depends on: #13401