Theorem Submodule.isOpenQuotientMap_mkQ

Modification history

2024-10-03 16:01
Mathlib/Topology/Algebra/Module/Basic.lean
feat(Topology/Group): drop an unneeded assumption (#16551) …
Added Submodule.isOpenQuotientMap_mkQView on Github →