Theorem properlyDiscontinuousSMul_iff

Modification history

2026-03-24 19:17

Mathlib/Topology/Algebra/ConstMulAction.lean

feat(Topology/Algebra/ProperAction): Fiberwise criterion for ProperSMul (#36904) …

Added properlyDiscontinuousSMul_iff View on Github →