IsCongruenceSubgroup — Mathlib

English

A congruence subgroup of SL(2, Z) is a subgroup that contains Gamma(N) for some nonzero N.

Русский

Конгруэнционная подгруппа SL(2, Z) — это подгруппа, содержащая Gamma(N) для какого-либо N ≠ 0.

LaTeX

$$$$ \text{IsCongruenceSubgroup}(\Gamma) \;\Longleftrightarrow\; \exists N \neq 0,\; \Gamma(N) \leq \Gamma. $$$$

Lean4

/-- A congruence subgroup is a subgroup of `SL(2, ℤ)` which contains some `Gamma N` for some
`N ≠ 0`. -/
def IsCongruenceSubgroup (Γ : Subgroup SL(2, ℤ)) : Prop :=
  ∃ N ≠ 0, Gamma N ≤ Γ

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