mem_Gamma_one

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

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

English

Any γ ∈ SL(2, Z) is in Gamma(1).

Русский

Любой элемент γ ∈ SL(2, Z) принадлежит Gamma(1).

LaTeX

$$γ ∈ Γ(1)$$

Lean4

theorem mem_Gamma_one (γ : SL(2, ℤ)) : γ ∈ Γ(1) := by simp only [Gamma_one_top, Subgroup.mem_top]

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

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

Разделы

Аффилиация

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