Gamma1 — Mathlib

English

Gamma1(N) is the congruence subgroup of SL(2, Z) consisting of matrices whose bottom row is congruent to (0,1) modulo N.

Русский

Γ1(N) является конгруэнтной подгруппой SL(2, Z), состоящей из матриц, чья нижняя строка совпадает с (0,1) по модулю N.

LaTeX

$$$$ \Gamma_1(N) = \{ A \in SL(2,\mathbb{Z}) : (A_{2,1}, A_{2,2}) \equiv (0,1) \pmod{N} \}. $$$$

Lean4

/-- The congruence subgroup `Gamma1` of `SL(2, ℤ)` consisting of matrices
whose bottom row is congruent to `(0,1)` modulo `N`. -/
def Gamma1 (N : ℕ) : Subgroup SL(2, ℤ) :=
  Subgroup.map ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⊤

Похожие утверждения