Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsClosed.smul_right_of_isCompact
Modification history
2025-11-05 17:11
Mathlib/Topology/Algebra/ProperAction/Basic.lean
feat: generalize `IsClosed.vadd_right_of_isCompact` to proper actions (#29715) …
Added
IsClosed.smul_right_of_isCompact
View on Github →