Theorem IsModuleTopology.continuous_of_linearMap

Modification history

2024-11-14 01:17
Mathlib/Topology/Algebra/Module/ModuleTopology.lean
feat(Topology/Algebra/Module): linear maps are continuous for the module topology (#18077) …
Added IsModuleTopology.continuous_of_linearMapView on Github →