Theorem IsModuleTopology.isOpenQuotientMap_of_surjectiveₛₗ

Modification history

2025-11-24 11:02
Mathlib/Topology/Algebra/Module/ModuleTopology.lean
feat(Topology): generalize `IsModuleTopology` lemmas to semilinear maps (#31429)
Added IsModuleTopology.isOpenQuotientMap_of_surjectiveₛₗView on Github →