Gamma_cong_eq_self

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

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

English

Conjugates of SL(2, Z) by GL(2, Q) are arithmetic subgroups.

Русский

Конъгруированные подгруппы SL(2, Z) по GL(2, Q являются арифметическими подгруппами.

LaTeX

$$$$ \text{congGL}(\text{Γ}, g) \text{ is arithmetic for } g \in GL(2,\mathbb{Q}). $$$$

Lean4

theorem Gamma_cong_eq_self (N : ℕ) (g : ConjAct SL(2, ℤ)) : g • Gamma N = Gamma N := by
  apply Subgroup.Normal.conjAct (Gamma_normal N)

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

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

Разделы

Аффилиация

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