Prove2Me

The rational prime lies in the maximal ideal of the C_p integers

Proved
PadicComplexInt.natCast_prime_mem_maximalIdeal

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

number-theoryp-adic-numbersvaluation-rings

The rational prime p belongs to the maximal ideal of the valuation ring of C_p.

Preamble
import Definitions.Def_KN_SeededThetaConstruction
import Mathlib.RingTheory.LocalRing.ResidueField.Basic

set_option autoImplicit false
noncomputable section
Formal statement
/-- The rational prime `p` lies in the maximal ideal of the valuation ring of
`ℂ_p`. -/
theorem PadicComplexInt.natCast_prime_mem_maximalIdeal
    (p : ℕ) [Fact p.Prime] :
    (p : 𝓞_ℂ_[p]) ∈ IsLocalRing.maximalIdeal (𝓞_ℂ_[p]) := by sorry
Source
Standard p-adic valuation theory.

View graph