Theorem Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom

Modification history

2025-12-22 22:40
Mathlib/Topology/Covering/Quotient.lean
feat: covering maps from properly discontinuous actions and discrete subgroups (#7596)
Added Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHomView on Github →