Theorem Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquiv

Modification history

2025-10-14 22:19
Mathlib/Topology/Algebra/IsUniformGroup/DiscreteSubgroup.lean
feat(Topology/Algebra): discrete iff finite index subgroup discrete (#29743) …
Added Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquivView on Github →