Prime Hecke recurrence for MTT eigenforms

Proved

MTT.Eigenform.hecke_recurrence

by davidloeffler · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

hecke-operatorsmodular-formsnumber-theoryq-expansions

Let $f$ be an MTT eigenform of weight $k$ . For a prime $q$ and every $m\geq 0$ , its Fourier coefficients satisfy the standard Hecke recurrence

a_{qm}(f)+\varepsilon_f(q)q^{k-1}\,\mathbf 1_{q\mid m} a_{m/q}(f)=a_q(f)a_m(f).

Preamble

import Definitions.Def_MTT_Arithmetic

set_option autoImplicit false
noncomputable section

Formal statement

/-- The Fourier coefficients of an MTT eigenform satisfy the usual prime
Hecke recurrence. -/
theorem MTT.Eigenform.hecke_recurrence
    {N k : ℕ} (hN : 0 < N)
    (ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι)
    (q : ℕ) (hq : q.Prime) (m : ℕ) :
    f.coeff (q * m) + f.epsilon q * (q : MTT.Qbar) ^ (k - 1) *
        (if q ∣ m then f.coeff (m / q) else 0) =
      f.coeff q * f.coeff m := by
  sorry

Source

The standard formula for the action of the prime Hecke operator on q-expansions.

View graph