instFiniteIndexGamma0

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

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

English

Gamma0(N) has finite index for NeZero N.

Русский

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

LaTeX

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

Lean4

instance instFiniteIndexGamma0 [NeZero N] : (Gamma0 N).FiniteIndex :=
  (Gamma0_is_congruence N).finiteIndex

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

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

Разделы

Аффилиация

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