instFiniteCuspOrbitsOfIsArithmetic

Mathlib.NumberTheory.ModularForms.Cusps

URI: https://scilib.ai/kg/mathlib#instFiniteCuspOrbitsOfIsArithmetic

← MathLib Explorer

English

An arithmetic subgroup 𝒢 has finitely many cusp orbits.

Русский

Арифметическая подгруппа имеет конечное число cusp-орбит.

LaTeX

$$$\\text{Finite}(\\mathrm{CuspOrbits}(\\mathcal{G}))$$$

Lean4

/-- An arithmetic subgroup has finitely many cusp orbits. -/
instance (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] : Finite (CuspOrbits 𝒢) :=
  .of_surjective _ (surjective_cosetToCuspOrbit 𝒢)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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