LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every irreducible element of a principal ideal domain is prime

Statement

Every irreducible element of a principal ideal domain is prime.

Facts & Assumptions

Given: A PID $R$ , an irreducible $p \in R$ , the irreducible and prime element definitions of Irreducible and prime elements of an integral domain, and maximal and prime ideals as in Prime ideals and maximal ideals in a commutative ring.

[F1]

In a PID, there is an $a \in R$ with $I = (a)$ for every ideal $I$ (Principal ideal domain).

[L1]

Every maximal ideal in a commutative unital ring is prime (Every maximal ideal of a commutative ring is prime).

Proof

technique · direct

1.1F1givenalgebra

Let $(p) \subseteq I \subseteq R$ . By [F1], write $I = (a)$ , so $p = a b$ for some $b$ . Irreducibility makes $a$ or $b$ a unit. If $a$ is a unit, $I = R$ ; if $b$ is a unit, $(a) = (p)$ . Since $p$ is a nonzero nonunit, $(p)$ is proper and therefore maximal.

2.1step 1.1L1

By [L1], the maximal ideal $(p)$ is prime.

3.1step 2.1given∎

If $p ∣ x y$ , then $x y \in (p)$ , so primality of the ideal gives $x \in (p)$ or $y \in (p)$ , equivalently $p ∣ x$ or $p ∣ y$ . Thus $p$ is a prime element. Associates generate the same ideal and give the same conclusion.

Depends on

Used by

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

K. Conrad, Modules over a PID, preliminary PID facts (standard reference, not scraped)
M. Brussel, Finitely Generated Modules over a PID, Section 1 (standard reference, not scraped)