Gamma0_is_congruence — Mathlib

English

Gamma0(N) is a congruence subgroup for any N ≠ 0, deduced from Gamma1 and its relation to Gamma1′.

Русский

Gamma0(N) является конгруэнтной подгруппой для любого N ≠ 0, выводится из Γ1 и связи с Γ1′.

LaTeX

$$$$ \forall N \,(N \neq 0) \Rightarrow \text{IsCongruenceSubgroup}(\Gamma_0(N)). $$$$

Lean4

theorem Gamma0_is_congruence (N : ℕ) [NeZero N] : IsCongruenceSubgroup (Gamma0 N) :=
  isCongruenceSubgroup_trans _ _ (Gamma1_in_Gamma0 N) (Gamma1_is_congruence N)

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