$\eta(\tau+1)=e^{2\pi i/24}\eta(\tau)$

Proved

TongString.dedekindEta_add_one

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

dedekind-etamodular-formsstring-theory

For every $\tau\in\mathbb C$ with $\operatorname{Im}\tau>0$ , the Dedekind eta function satisfies

\eta(\tau+1)=e^{2\pi i/24}\,\eta(\tau).

This is the behaviour of $\eta$ under the modular transformation $T:\tau\mapsto\tau+1$ .

Preamble

import Mathlib
import Definitions.Def_TongString_dedekind_eta

Formal statement

namespace TongString

open Complex

theorem dedekindEta_add_one (τ : ℂ) (hτ : 0 < τ.im) :
    dedekindEta (τ + 1) = Complex.exp (2 * Real.pi * I / 24) * dedekindEta τ := by sorry

end TongString

Source

D. Tong, *String Theory*, University of Cambridge Part III Mathematical Tripos lecture notes (January 2009), http://www.damtp.cam.ac.uk/user/tong/string.html, Section 6.4.2, p. 151 ('The eta-function satisfies the identities η(τ+1) = e^{2πi/24} η(τ) ...')

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic), non-blind: same agent that drafted the statement

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source text and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; a reviewer should compare the Lean code against the source directly.

For every complex number $\tau$ with $\operatorname{Im}\tau>0$ , the statement asserts

\eta(\tau+1)=e^{2\pi i/24}\,\eta(\tau),

where $\eta$ is the imported function $\eta(\tau)=e^{2\pi i\tau/24}\prod_{m\ge1}\bigl(1-e^{2\pi i m\tau}\bigr)$ , the product being an unconditional infinite product in $\mathbb C$ (defined as $1$ if not unconditionally convergent), and $e^{2\pi i/24}$ is the complex exponential.

View graph

η(τ+1)=e2πi/24η(τ)\eta(\tau+1)=e^{2\pi i/24}\eta(\tau)η(τ+1)=e2πi/24η(τ)

$\eta(\tau+1)=e^{2\pi i/24}\eta(\tau)$