Theorem Subgroup.discreteTopology

Modification history

2024-09-12 09:29
Mathlib/Topology/Algebra/OpenSubgroup.lean
feat(Algebra/OpenSubgroup): quotient of compact group by open subgroup is finite (#16671) …
Added Subgroup.discreteTopologyView on Github →