Prove2Me

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

Proved
MTT.Eigenform.coefficientPrime_isPrime

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

modular-formsnumber-fieldsnumber-theoryp-adic-numbers

The ideal of the eigenform coefficient ring selected by an embedding into Cp\mathbf C_p is a prime ideal.

Preamble
import Definitions.Def_MTT_EigenformCoefficientPrime

set_option autoImplicit false
noncomputable section
Formal statement
/-- The prime selected by a `p`-adic embedding is a prime ideal. -/
theorem MTT.Eigenform.coefficientPrime_isPrime
    {N k p : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (f : MTT.Eigenform N k ι) (ιp : MTT.Qbar →+* ℂ_[p]) :
    (f.coefficientPrime ιp).IsPrime := by
  sorry
Source
Prime ideals pull back along ring homomorphisms; the maximal ideal of the valuation ring of C_p is prime.

View graph