eta_q_eq_cexp

Mathlib.NumberTheory.ModularForms.DedekindEta

URI: https://scilib.ai/kg/mathlib#ModularForm.eta_q_eq_cexp

← MathLib Explorer

English

The cusps of SL(2,ℤ) are exactly the rational points range.

Русский

cusp SL(2,ℤ) точно совпадает с рациональными точками.

LaTeX

$$$IsCusp(c, \\mathcal{S L}) \\iff c \\in \\operatorname{range}(\\mathrm{OnePoint.map}(\\mathrm{Rat.cast}))$$$

Lean4

theorem eta_q_eq_cexp (n : ℕ) (z : ℂ) : eta_q n z = cexp (2 * π * I * (n + 1) * z) :=
  by
  simp [eta_q, Periodic.qParam, ← Complex.exp_nsmul]
  ring_nf

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

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

Разделы

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

Аффилиация

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