Commit 2024-11-14 01:17 3d1af1d0

feat(Topology/Algebra/Module): linear maps are continuous for the module topology (#18077) If M and N are modules over a topological ring and if we give them both the module topology, then any linear map from M to N is automatically continuous. More generally if M has the module topology and N is any topological module, all linear maps from M to N are continuous. From the FLT project.