Commit 2023-05-24 09:57 30e138d1

View on Github →

feat: port NumberTheory.ModularForms.CongruenceSubgroups (#4296)

Estimated changes

added def Gamma0
added def Gamma0Map
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 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