Theorem Subgroup.quotient_finite_of_isOpen

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.quotient_finite_of_isOpenView on Github →