Commit 2025-10-14 22:19 37ee77cc

View on Github →

feat(Topology/Algebra): discrete iff finite index subgroup discrete (#29743) Show that if G is a topological group and H is a finite-index subgroup, then H is discrete iff G is. As application, show that arithmetic subgroups of GL(2, R), which are by definition those commensurable with SL(2, Z), are discrete.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Constructions.lean

added theorem Set.biUnion_empty_finset

Modified Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added def ContinuousMulEquiv.Simps.symm_apply

added theorem MulEquiv.symm_toContinuousMulEquiv

added def MulEquiv.toContinuousMulEquiv

added theorem MulEquiv.toHomeomorph_toContinuousMulEquiv

added theorem MulEquiv.toMulEquiv_toContinuousMulEquiv

Created Mathlib/Topology/Algebra/IsUniformGroup/DiscreteSubgroup.lean

added theorem Subgroup.Commensurable.discreteTopology_iff

added theorem Subgroup.discreteTopology_iff_of_finiteIndex

added theorem Subgroup.discreteTopology_iff_of_isFiniteRelIndex

added def Subgroup.subgroupOfContinuousMulEquivOfLe

added theorem Subgroup.subgroupOfContinuousMulEquivOfLe_symm_apply

added theorem Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquiv

Modified Mathlib/Topology/Constructions.lean

deleted theorem discreteTopology_subtype_iff

Modified Mathlib/Topology/DiscreteSubset.lean

added theorem compl_mem_codiscrete_iff

added theorem discreteTopology_biUnion_finset

added theorem discreteTopology_iUnion_fintype

added theorem discreteTopology_subtype_iff'

added theorem discreteTopology_subtype_iff

added theorem discreteTopology_union

Modified Mathlib/Topology/Homeomorph/Defs.lean

added theorem Equiv.symm_toHomeomorph

deleted theorem Equiv.toHomeomorph_symm