TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

Eisenstein criterion over the integers

Statement

Let $f=a_nx^n+\cdots+a_0\in\mathbb Z[x]$ be primitive with $n\ge1$ . If there is a prime $p$ such that

$p\nmid a_n,\qquad p\mid a_i\ \text{for every }i<n,\qquad p^2\nmid a_0,$

then $f$ is irreducible in $\mathbb Q[x]$ .

Facts & Assumptions

Given: A primitive polynomial $f=a_nx^n+\cdots+a_0$ and a prime $p$ satisfying the displayed divisibility conditions.

[L1]

A rational factorization of a primitive integer polynomial clears to a primitive integer factorization (Gauss lemma: primitive factorisations over $\mathbb Q$ can be cleared to primitive factorisations over $\mathbb Z$ ).

[L2]

Polynomial rings over fields are unique factorisation domains, hence domains (For every field $F$ , $F[x]$ is a unique factorisation domain).

[L3]

Reduction of coefficients modulo $p$ is a polynomial-ring homomorphism (Universal property of $R[x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[L4]

The ring $\mathbb Z/p$ is the quotient $\mathbb Z/p\mathbb Z$ (For every $n\in\mathbb N$ , the congruence-class ring $\mathbb Z/n$ is the quotient ring $\mathbb Z/n\mathbb Z$ ).

[L5]

A prime $p$ is greater than $1$ and its only positive divisors are $1,p$ (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L6]

The ring $\mathbb Z/p$ is a field (For every prime $p$ , the two operations on $\mathbb{Z}/p$ make it a field).

Proof

technique · contradiction

1.1

Suppose for contradiction that $f$ is reducible over $\mathbb Q$ ; [L1] gives $f=GH$ with primitive integer polynomials $G,H$ of positive degree.

assume-contragivenL1

2.1

By [L3] and [L4], reduction modulo $p$ gives $\bar G\bar H=\bar a_nx^n$ in the domain $(\mathbb Z/p)[x]$ of [L6] and [L2]. Because $p\nmid a_n$ , the leading coefficients of $G$ and $H$ both survive reduction: their product is $a_n$ , so neither is divisible by $p$ . Thus $\deg\bar G=\deg G>0$ and $\deg\bar H=\deg H>0$ . Comparing the least nonzero terms in the product $\bar a_nx^n$ now shows that both reductions are monomials of positive degree, so the constant coefficients of $G$ and $H$ are divisible by $p$ .

step 1.1L2L3L4L5L6algebra

3.1

The constant coefficient $a_0$ is the product of those two constant coefficients, so step 2.1 gives $p^2\mid a_0$ , contradicting the hypothesis; hence $f$ is irreducible over $\mathbb Q$ .

step 2.1L5discharge-contradiction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 112 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Thomas W. Judson, Abstract Algebra: Theory and Applications, Theorem 17.17 (standard reference, not scraped)
Keith Conrad, Irreducibility Tests in Q[T], Appendix A.4 (standard reference, not scraped)