Principal_Ideal_of_PID_Irreducible_iff_Maximal

Proved

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

irreduciblemaximal-idealprincipal-ideal-domainproofwikiring-theory

Let $\struct {D, +, \circ}$ be a principal ideal domain. Let $\ideal p$ be the principal ideal of $D$ generated by $p$ . Then $p$ is irreducible $\ideal p$ is a maximal ideal of $D$ .

Preamble

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

Formal statement

theorem Principal_Ideal_of_PID_Irreducible_iff_Maximal {D : Type _} [CommRing D] [IsDomain D] [IsPrincipalIdealRing D] (p : D) (hp : p ≠ 0) : Irreducible p ↔ (Ideal.span ({p} : Set D)).IsMaximal := by sorry

Source

https://proofwiki.org/wiki/Principal_Ideal_of_Principal_Ideal_Domain_is_of_Irreducible_Element_iff_Maximal

View graph