Prove2Me

The coefficient prime selected by a p-adic embedding is maximal

Proved
MTT.Eigenform.coefficientPrime_isMaximal

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

modular-formsnumber-fieldsnumber-theoryp-adic-numbers

For an eigenform of positive level and weight at least two, the nonzero prime ideal of its coefficient ring selected by a pp-adic embedding is maximal.

Preamble
import Theorems.Thm_MTT_Eigenform_coefficientPrime_isPrime
import Theorems.Thm_MTT_Eigenform_coefficientPrime_ne_bot
import Theorems.Thm_MTT_numberField_coefficientField
import Mathlib.RingTheory.DedekindDomain.Basic

set_option autoImplicit false
noncomputable section

open NumberField
Formal statement
/-- The prime selected by a `p`-adic embedding is a maximal ideal of the
integer ring of the coefficient field. -/
theorem MTT.Eigenform.coefficientPrime_isMaximal
    {N k p : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (f : MTT.Eigenform N k ι) (ιp : MTT.Qbar →+* ℂ_[p]) :
    (f.coefficientPrime ιp).IsMaximal := by
  sorry
Source
The ring of integers of a number field is a Dedekind domain, in which every nonzero prime ideal is maximal.

View graph