Theorem Subgroup.isClosed_of_isDiscrete

Modification history

2026-09-09 21:26
Mathlib/Topology/Algebra/OpenSubgroup.lean
feat: a locally closed subgroup is closed (#42501) …
Added Subgroup.isClosed_of_isDiscreteView on Github →