Theorem Subgroup.discreteTopology

Modification history

2026-03-13 18:00
Mathlib/Topology/Algebra/OpenSubgroup.lean
feat: generalize some `ContinuousMul` hypotheses to `SeparatelyContinuousMul` (#36562) …
Modified Subgroup.discreteTopologyView on Github →
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 →