eta

Mathlib.NumberTheory.ModularForms.DedekindEta

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

← MathLib Explorer

English

η_q(n,z) = e^{2π i (n+1) z}; equivalently, η_q(n,z) = q^{n+1} with q = e^{2π i z}.

Русский

η_q(n,z) = e^{2π i (n+1) z}; эквивалентно η_q(n,z) = q^{n+1} с q = e^{2π i z}.

LaTeX

$$$\\eta_q(n,z) = e^{2 \\pi i (n+1) z}$$$

Lean4

/-- The eta function, whose value at z is `q^ 1 / 24 * ∏' 1 - q ^ (n + 1)` for `q = e ^ 2 π i z`. -/
noncomputable def eta (z : ℂ) :=
  𝕢 24 z * ∏' n, (1 - eta_q n z)

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

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

Разделы

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

Аффилиация

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