Extensions to Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

The Subgroup.width API and Gamma_width formerly hosted here also live in the companion file LeanPool.LeanModularForms.ForMathlib.CongruenceSubgrps, which is the canonical one inside this project. This file kept its own copy of the same definitions under the original "Copy" filename, but to avoid clashing redeclarations of Subgroup.width etc. in the project-wide mk_all index, we now import the canonical companion and add only the genuinely-local extras (mem_conjGL', finiteIndex_conjGL' — the generalisation of Mathlib.CongruenceSubgroup.finiteIndex_conjGL to an arbitrary finite-index Γ).

theorem CongruenceSubgroup.mem_conjGL' {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {g : GL (Fin 2) ℝ} {x : Matrix.SpecialLinearGroup (Fin 2) ℤ} : x ∈ conjGL Γ g ↔ ∃ y ∈ Γ, g⁻¹ * Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) y) * g = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) x)

theorem CongruenceSubgroup.finiteIndex_conjGL' (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] (g : GL (Fin 2) ℚ) : (conjGL Γ ((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ)) g)).FiniteIndex

If Γ has finite index in SL(2, ℤ), then so does g⁻¹ Γ g ∩ SL(2, ℤ) for any g ∈ GL(2, ℚ). (This generalises Mathlib's finiteIndex_conjGL, which only covers Γ = ⊤.)