Mathlib Changelog
v4
Changelog
About
Github
Theorem
ProperlyDiscontinuousSMul.exists_nhds_disjoint_image
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_disjoint_image
View on Github →