The rational prime belongs to the selected coefficient prime

Proved

MTT.Eigenform.p_mem_coefficientPrime

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

modular-formsnumber-fieldsnumber-theoryp-adic-numbers

Let $f$ be an MTT eigenform and let $\iota_p:\overline{\mathbf Q}\hookrightarrow\mathbf C_p$ select the prime $\lambda_{\iota_p}$ of its coefficient field. Then the rational integer $p$ belongs to $\lambda_{\iota_p}$ .

Preamble

import Definitions.Def_MTT_EigenformCoefficientPrime

set_option autoImplicit false
noncomputable section

open NumberField

Formal statement

/-- The rational prime `p` belongs to the coefficient-field prime selected by
a `p`-adic embedding. -/
theorem MTT.Eigenform.p_mem_coefficientPrime
    {N k p : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (f : MTT.Eigenform N k ι) (ιp : MTT.Qbar →+* ℂ_[p]) :
    (p : 𝓞 f.coefficientField) ∈ f.coefficientPrime ιp := by
  sorry

Source

The standard prime ideal selected by a p-adic embedding, together with the identity |p|_p < 1.

View graph