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_isOpen'View on Github →