Theorem MulAction.isOpenQuotientMap_quotientMk

Modification history

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