The coefficient field of an eigenform is a number field

Proved

MTT.numberField_coefficientField

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

eigenformsmodular-formsnumber-fields

Let $f$ be an MTT eigenform of positive level $N$ and weight $k \ge 2$ . Its coefficient field $K_f$ , generated over $\mathbb Q$ by all Fourier coefficients and all values of the nebentype, is a number field:

[K_f : \mathbb Q] < \infty.

This packages finite-dimensionality into Mathlib's standard NumberField predicate, making the arithmetic of its integer ring and residue fields directly available.

Preamble

import Definitions.Def_MTT_EigenformCoefficientField
import Mathlib.NumberTheory.NumberField.Basic

set_option autoImplicit false
noncomputable section

Formal statement

theorem MTT.numberField_coefficientField
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι) :
    NumberField f.coefficientField := by sorry

Source

Standard consequence of finite-dimensionality of the coefficient field over ℚ; see Diamond–Shurman, A First Course in Modular Forms, §5.8.

View graph