instFiniteIndexGamma1

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

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

English

Gamma1(N) has finite index for NeZero N.

Русский

Gamma1(N) имеет конечный индекс при N ≠ 0.

LaTeX

$$$$ (\text{NeZero } N) \Rightarrow (\Gamma_1(N)).\text{FiniteIndex}. $$$$

Lean4

instance instFiniteIndexGamma1 [NeZero N] : (Gamma1 N).FiniteIndex :=
  (Gamma1_is_congruence N).finiteIndex

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

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

Разделы

Аффилиация

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