Commit 2025-05-24 20:33 b916162c

View on Github →

feat(NumberTheory/ModularForms): Conjugation by GL(2, Q) preserves congruence subgroups (#24740) Show that the conjugate by GL(2, Q) of a finite-index (resp. congruence) subgroup of SL(2, Z) is a finite-index (resp. congruence) subgroup.

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

added theorem AddSubgroup.relindex_pointwise_smul

added theorem Subgroup.relindex_comap_ne_zero

added theorem Subgroup.relindex_inter_ne_zero

added theorem Subgroup.relindex_pointwise_smul

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

added def Matrix.SpecialLinearGroup.mapGL

added theorem Matrix.SpecialLinearGroup.mapGL_coe_matrix

added theorem Matrix.SpecialLinearGroup.mapGL_inj

added theorem Matrix.SpecialLinearGroup.mapGL_injective

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

added theorem CongruenceSubgroup.IsCongruenceSubgroup.conjGL

added theorem CongruenceSubgroup.exists_Gamma_le_conj'

added theorem CongruenceSubgroup.exists_Gamma_le_conj

added theorem CongruenceSubgroup.finiteIndex_conjGL