Namespace CongruenceSubgroup 27 theorems
- 1 is a strict period of Γ₀(N)
CongruenceSubgroup.one_mem_strictPeriods_Gamma00 below · cited by 46 · depth 9 - Relative index of Γ₁(M)∩Γ₀(Mq) in Γ₁(M)
CongruenceSubgroup.relIndex_gamma1_inf_gamma0_mul_of_dvd0 below · cited by 3 · depth 14 - Γ₀(M) lies in the subgroup generated by T and q∣ b
CongruenceSubgroup.Gamma0_le_closure_T_union_setOf_dvd0 below · cited by 1 · depth 15 - Γ(N/p) inside Γ₁(N)∩Γ(M) with a lower unipotent
CongruenceSubgroup.Gamma_div_le_gamma1_inf_Gamma_sup_zpowers0 below · cited by 1 · depth 16 - A transversal of ±Γ in SL₂(ℤ) adapted to T and S
CongruenceSubgroup.exists_finset_transversal_adapted_T_S0 below · cited by 1 · depth 17 - First-column criteria for ±Γ₁(N)-membership
CongruenceSubgroup.mem_or_neg_mem_Gamma1_iff_and_exists_T_zpow_S_inv_iff0 below · cited by 1 · depth 18 - Reduction of Γ(N) onto SL₂(𝔽ₚ) for p ∤ N
CongruenceSubgroup.exists_mem_Gamma_map_eq_of_not_dvd0 below · cited by 24 · depth 19 - Transfer identity: parabolic values of φ on Γ₀(N) sum to zero
CongruenceSubgroup.finsum_addMonoidHom_conj_T_zpow_eq_zero0 below · cited by 1 · depth 19 - Γ₀(3) is generated by T, U and -1
CongruenceSubgroup.closure_T_U_neg_one_eq_Gamma0_three0 below · cited by 1 · depth 20 - Γ₁(N)∩Γ₀(ℓ)=Γ₁(N)∩Γ₀(Nℓ) for coprime levels
CongruenceSubgroup.gamma1_inf_gamma0_eq_gamma1_inf_gamma0_mul_of_coprime0 below · cited by 1 · depth 20 - Γ₁(N)∩Γ₀(Nℓ)=Γ_H(Nℓ) for H the reduction kernel
CongruenceSubgroup.gamma1_inf_gamma0_mul_eq_gammaH_ker0 below · cited by 2 · depth 20 - i∞ is a cusp of Γ₁(M) in GL₂(ℝ)
CongruenceSubgroup.isCusp_infty_gamma1_mapGL0 below · cited by 1 · depth 20 - Index and cusp count of Γ₁(Mp) versus Γ₁(M)
CongruenceSubgroup.index_gamma1_mul_and_natCard_doubleCoset_gamma1_mul_of_prime_of_not_dvd7 below · cited by 2 · depth 22 - Index of Γ₁(Mp) for p∤ M
CongruenceSubgroup.index_gamma1_mul_eq_of_prime_of_not_dvd1 below · cited by 2 · depth 23 - Index of ±Γ₁(M) and elliptic double-coset counts
CongruenceSubgroup.index_gamma1_sup_zpowers_neg_one_eq_three_mul_natCard_doubleCoset_and_eq_two_mul0 below · cited by 6 · depth 23 - Regularity of the cusps of Γ₁(N) for N ≥ 5
CongruenceSubgroup.natCard_doubleCoset_gamma1_map_T_eq_two_mul_of_five_le0 below · cited by 1 · depth 23 - Multiplicativity of the Γ₁–⟨ T⟩ double-coset count in coprime levels
CongruenceSubgroup.natCard_doubleCoset_gamma1_map_T_mul_of_coprime0 below · cited by 1 · depth 23 - Double cosets of the reduced Γ₁(p) and ⟨ T⟩ number 2(p-1)
CongruenceSubgroup.natCard_doubleCoset_gamma1_map_T_of_prime0 below · cited by 1 · depth 23 - Adjoining -1 halves the index of Γ₁(N), N≥ 3
CongruenceSubgroup.two_mul_index_gamma1_sup_zpowers_neg_one0 below · cited by 2 · depth 23 - Elements of ±Γ₁(M), M ≥ 4, fixing a point of H
CongruenceSubgroup.eq_one_or_eq_neg_one_of_mem_Gamma1_of_smul_eq0 below · cited by 2 · depth 24 - Index p-1 of ±Γ₁(Mp) in ±(Γ₁(M)∩Γ₀(p))
CongruenceSubgroup.relIndex_gamma1_mul_sup_zpowers_neg_one_gamma1_inf_gamma0_eq_sub_one0 below · cited by 1 · depth 27 - Diamond lift: prescribed entry in Γ(q)∩Γ₀(M')
CongruenceSubgroup.exists_mem_Gamma_mem_Gamma0_intCast_apply_eq_of_coprime_of_dvd1 below · cited by 4 · depth 29 - Approximation of SL₂(ℤ) modulo q inside Γ(ℓ)∩Γ₀(M')
CongruenceSubgroup.exists_mem_Gamma_mem_Gamma0_mul_inv_mem_Gamma_of_not_dvd2 below · cited by 6 · depth 31 - Regularity of the cusps of Γ₁(M) for M ∤ 4
CongruenceSubgroup.conj_T_zpow_mem_Gamma1_of_mem_sup_zpowers_neg_one0 below · cited by 1 · depth 32 - Index of ±(Γ∩Γ₀(Lℓ)) for Γ₁(L)≤Γ≤Γ₀(L)
CongruenceSubgroup.index_inf_gamma0_mul_sup_zpowers_neg_one_of_gamma1_le_of_le_gamma0202 below · cited by 1 · depth 32 - Generation of Γ(q)∩Γ₀(M') modulo Γ(qℓ)
CongruenceSubgroup.exists_list_forall_eq_T_zpow_or_conj_and_mul_prod_inv_mem_Gamma_mul_of_mem_Gamma_of_mem_Gamma02 below · cited by 1 · depth 33 - Relative index of Γ₀(Np) in Γ₀(N) is p+1
CongruenceSubgroup.relIndex_gamma0_mul_of_prime_of_not_dvd199 below · cited by 1 · depth 33