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.
For every prime and positive , is irreducible over
Statement
For every prime integer and every positive natural number , the polynomial is irreducible in .
Facts & Assumptions
Given: A prime integer and a natural number .
A primitive integer polynomial is irreducible over when a prime divides every nonleading coefficient, does not divide the leading coefficient, and its square does not divide the constant coefficient (Eisenstein criterion over the integers).
A prime integer satisfies and has no positive divisor other than (Prime and composite integers: is prime when and its only positive divisors are and ).
Nonzero integers cancel in products (The integers have no zero divisors; multiplicative cancellation).
The only integer units are and ( is a commutative monoid whose group of units is ; equivalently holds exactly for and ).
Proof
The polynomial is primitive because its leading coefficient is the unit from [L4]; the prime divides every nonleading coefficient, including the zero intermediate coefficients, and does not divide .
If divided , cancellation by the nonzero using [L3] would make a unit, contradicting [L2] and [L4]; thus Eisenstein's criterion [L1] applies and proves irreducibility.
Depends on
- Eisenstein criterion over the integers
- Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$
- The integers have no zero divisors; multiplicative cancellation
- $(\mathbb{Z}, \cdot, 1)$ is a commutative monoid whose group of units is $\{1, -1\}$; equivalently $u \mid 1$ holds exactly for $u = 1$ and $u = -1$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 84 results over 24 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
- Keith Conrad, Irreducibility Tests in Q[T], Example 1.6 (standard reference, not scraped)