Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

For a nonconstant p in F[x], the ideal (p) is maximal and F[x]/(p) is a field exactly when p is irreducible

Statement

Let F be a field and let p∈F[x] be nonconstant. The following are equivalent:

  1. p is irreducible;
  2. the principal ideal (p) is maximal;
  3. the quotient ring F[x]/(p) is a field.

Facts & Assumptions

Given: A field F and a nonconstant polynomial p∈F[x].

[L1]

The monic gcd of two polynomials is a polynomial linear combination of them (Bézout identity and the Euclidean algorithm for polynomials over a field).

[L2]

The principal ideal (p) is the smallest ideal containing p (The ideal generated by a subset and principal ideals).

[L3]

A maximal ideal is a proper ideal with no proper ideal strictly between it and the whole ring (Prime ideals and maximal ideals in a commutative ring).

[L4]

In the quotient ring R/I, multiplication is (r+I)(s+I)=rs+I (The quotient ring R/I with (r+I)(s+I)=rs+I).

[L5]

For a commutative ring R, the quotient R/M is a field if and only if M is maximal (R/M is a field if and only if M is a maximal ideal).

[L6]

An irreducible element is a nonzero nonunit with no factorization into two nonunits (Irreducible and prime elements of an integral domain).

Proof

technique · direct
1.1

In a commutative ring the multiples of p form an ideal containing p and lie in every ideal containing p, so [L2] identifies (p) with the set of multiples of p. Suppose p is irreducible and f+(p) is a nonzero residue class; then p∤f. If a common divisor d of p,f were a nonunit, a factorization p=de and [L6] would make e a unit, so d would be associate to p and d∣f would imply p∣f, a contradiction. Thus every common divisor is a unit, and [L1] gives Ap+Bf=1, whence [L4] gives (B+(p))(f+(p))=1+(p); every nonzero class is invertible, so the quotient is a field.

givenL1L2L4L6algebra
2.1

Conversely, suppose the quotient is a field and p=ab. By [L4], the two residue classes have product zero, so one is zero; say a∈(p). The characterization established in step 1.1 gives a=pc, and hence p=ab=pcb. A direct leading-coefficient argument shows that F[x] has no zero divisors, because F is a field, so cancellation of the nonzero polynomial p gives cb=1 and makes b a unit. The other case similarly makes a a unit, and [L6] makes p irreducible.

step 1.1givenL2L4L6algebra
3.1

Steps 1.1 and 2.1 prove that irreducibility is equivalent to quotient fieldness, and [L5] identifies quotient fieldness with maximality of (p) in the sense of [L3].

step 1.1step 2.1L3L5∎

Depends on

Used by

Dependency tree · two levels

20 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