Prime_Number_iff_Generates_Principal_Maximal_Ideal

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

idealsmaximal-idealprime-numbersproofwikiring-theory

Let $\Z_{>0}$ be the set of strictly positive integers. Let $p \in \Z_{>0}$ . Let $\ideal p$ be the principal ideal of $\Z$ generated by $p$ . Then $p$ is prime $\ideal p$ is a maximal ideal of $\Z$ .

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.RingTheory.PrincipalIdealDomain

Formal statement

theorem Prime_Number_iff_Generates_Principal_Maximal_Ideal (p : ℕ) (hp : 1 < p) : Nat.Prime p ↔ (Ideal.span ({(p : ℤ)} : Set ℤ)).IsMaximal := by sorry

Source

https://proofwiki.org/wiki/Prime_Number_iff_Generates_Principal_Maximal_Ideal

View graph