Theorem IsModuleTopology.continuous_of_distribMulActionHom

Modification history

2025-11-24 11:02
Mathlib/Topology/Algebra/Module/ModuleTopology.lean
feat(Topology): generalize `IsModuleTopology` lemmas to semilinear maps (#31429)
Modified IsModuleTopology.continuous_of_distribMulActionHomView on Github →
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_distribMulActionHomView on Github →