Theorems · Definition · number theory
CongruenceSubgroup.Gamma
ℕ → Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)
The full level N congruence subgroup of SL(2, ℤ) of matrices that reduce to the identity
modulo N.
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Subgroupstatement · cited by 3,593
- ZModproof · cited by 1,024
- Matrix.SpecialLinearGroupstatement · cited by 348
- Int.castRingHomproof · cited by 254
- MonoidHom.kerproof · cited by 212
- Matrix.SpecialLinearGroup.mapproof · cited by 77
Cited by36
Results whose statement or proof uses this declaration.
- EisensteinSeries.eisensteinSeriesSIFstatement and proof · cited by 8
- CongruenceSubgroup.IsCongruenceSubgroupproof · cited by 7
- CongruenceSubgroup.Gamma_one_topstatement · cited by 3
- EisensteinSeries.eisensteinSeriesSIF_applystatement · cited by 3
- CongruenceSubgroup.exists_Gamma_le_conj'statement and proof · cited by 2
- CongruenceSubgroup.mem_Gamma_onestatement · cited by 2
- CongruenceSubgroup.strictPeriods_Gammastatement · cited by 2
- CongruenceSubgroup.Gamma_one_coe_eq_SLstatement · cited by 2
- CongruenceSubgroup.exists_Gamma_le_conjstatement and proof · cited by 1
- CongruenceSubgroup.isCongruenceSubgroup_transproof · cited by 1
- SlashInvariantForm.T_zpow_width_invariantstatement and proof · cited by 1
- EisensteinSeries.eisensteinSeriesSIF_mdifferentiablestatement · cited by 1