Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-08 10:32 9b6eef6e

View on Github →

feat(number_theory/modular_forms/congruence_subgroups): Add definition of congruence subgroups. (#15159) This contains the definition of a congruence subgroup of SL(2,Z) and defines Gamma1, Gamma0 and full level subgroups. It also contains some basic results about them.

Estimated changes

added theorem matrix.two_mul_expl
added def Gamma0
added theorem Gamma0_det
added theorem Gamma0_is_congruence
added theorem Gamma0_mem
added def Gamma1'
added def Gamma1
added theorem Gamma1_in_Gamma0
added theorem Gamma1_is_congruence
added theorem Gamma1_mem'
added theorem Gamma1_mem
added theorem Gamma1_to_Gamma0_mem
added def Gamma
added def Gamma_0_map
added theorem Gamma_cong_eq_self
added theorem Gamma_is_cong_sub
added theorem Gamma_mem'
added theorem Gamma_mem
added theorem Gamma_normal
added theorem Gamma_one_top
added theorem Gamma_zero_bot
added theorem conj_cong_is_cong