Gamma1_in_Gamma0

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

URI: https://scilib.ai/kg/mathlib#CongruenceSubgroup.Gamma1_in_Gamma0

English

For every N, the Gamma1(N) subgroup is contained in Gamma0(N).

Русский

Для каждого N подгруппа Γ1(N) содержится в Γ0(N).

LaTeX

$$$$ \Gamma_1(N) \leq \Gamma_0(N). $$$$

Lean4

theorem Gamma1_in_Gamma0 (N : ℕ) : Gamma1 N ≤ Gamma0 N :=
  by
  intro x HA
  simp only [Gamma0_mem, Gamma1_mem] at *
  exact HA.2.2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru