Commit 2024-10-19 21:32 227950d6

feat: topology on module over topological ring (#16895) Given a module over a topological ring, we define the module topology on this module to be the finest module making it into a topological module (i.e. the finest topology making addition and scalar multiplication continuous). NB this PR gave rise to a discussion about whether ⨆ a ∈ s, f a or sSup (f '' s) should be the simp normal form, which was discussed on Zulip without any clear conclusion.