Theorem ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self

Modification history

2025-12-22 22:40
Mathlib/Topology/Algebra/ConstMulAction.lean
feat: covering maps from properly discontinuous actions and discrete subgroups (#7596)
Added ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_selfView on Github →