Theorems · Theorem · number theory

CongruenceSubgroup.exists_Gamma_le_conj

∀ (g : GL (Fin 2) ℚ) (M : ℕ) [NeZero M],
  ∃ N,
    N ≠ 0 ∧
      ∀ x ∈ CongruenceSubgroup.Gamma N,
        g * (Matrix.SpecialLinearGroup.mapGL ℚ) x * g⁻¹ ∈
          Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma M)

For any g ∈ GL(2, ℚ) and M ≠ 0, there exists N such that g x g⁻¹ ∈ Γ(M) for all x ∈ Γ(N).

Defined in

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Cited by

1 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZero