The selected coefficient prime is nonzero
ProvedMTT.Eigenform.coefficientPrime_ne_botmodular-formsnumber-fieldsnumber-theoryp-adic-numbers
The prime ideal of the eigenform coefficient field selected by a -adic embedding is not the zero ideal. Indeed, it contains the nonzero rational integer .
Preamble
import Theorems.Thm_MTT_Eigenform_p_mem_coefficientPrime set_option autoImplicit false noncomputable section
Formal statement
/-- The coefficient-field prime selected by a `p`-adic embedding is nonzero. -/
theorem MTT.Eigenform.coefficientPrime_ne_bot
{N k p : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
(f : MTT.Eigenform N k ι) (ιp : MTT.Qbar →+* ℂ_[p]) :
f.coefficientPrime ιp ≠ ⊥ := by
sorrySource
The standard prime ideal selected by a p-adic embedding, together with the identity |p|_p < 1.