English
Gamma0(N) consists of SL(2, Z) matrices whose lower-left entry is 0 modulo N.
Русский
Gamma0(N) состоит из матриц SL(2, Z), у которых нижний левый элемент равен 0 по модулю N.
LaTeX
$$Gamma0(N) = { A ∈ SL(2, Z) | A_{21} ≡ 0 (mod N) }$$
Lean4
/-- The congruence subgroup of `SL(2, ℤ)` of matrices whose lower left-hand entry reduces to zero
modulo `N`. -/
def Gamma0 : Subgroup SL(2, ℤ) where
carrier := {g | (g 1 0 : ZMod N) = 0}
one_mem' := by simp
mul_mem' := by
intro a b ha hb
simp only [Set.mem_setOf_eq]
have h := (Matrix.two_mul_expl a.1 b.1).2.2.1
simp only [coe_mul, Set.mem_setOf_eq] at *
rw [h]
simp [ha, hb]
inv_mem' := by
intro a ha
simp only [Set.mem_setOf_eq]
rw [SL2_inv_expl a]
simp only [cons_val_zero, cons_val_one, Int.cast_neg, neg_eq_zero, Set.mem_setOf_eq] at *
exact ha
