Alphabeta Math

Polynomial Rings, the Division Algorithm and Roots

About this page
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.

✓ 35 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 35 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Combinatorics
Number Theory
Real Analysis
Set Theory
2 · Logical flowchart

3 · Items

Definition

The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution

Lemma

Coefficientwise sums and convolution products of finitely supported sequences are finitely supported

Theorem

Polynomial convolution makes R[x] a commutative ring containing R as its constant subring

Definition

Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree

Proposition

Finitely supported coefficient sequences and trimmed finite coefficient lists define the same formal polynomials

Proposition

Degree inequalities for sums and products over a commutative ring

Theorem

Over an integral domain, degrees add under multiplication of nonzero polynomials

Corollary

A polynomial ring over an integral domain is an integral domain

Corollary

The units of R[x] over an integral domain are exactly the constant polynomials whose values are units of R

Definition

Evaluation and roots of a polynomial in a commutative target ring

Theorem

Universal property of R[x]: a coefficient homomorphism and the image of x determine a unique ring homomorphism

Definition

Polynomial rings in finitely many commuting indeterminates by iteration

Corollary

A polynomial ring in finitely many indeterminates over an integral domain is an integral domain

Theorem

Division by a monic polynomial over a commutative ring

Corollary

Factor theorem over a commutative ring

Theorem

Division algorithm for polynomials over a field

Corollary

For every field F, F[x] is a Euclidean domain with degree as Euclidean function

Corollary

For every field F, F[x] is a principal ideal domain

Definition

The monic greatest common divisor of two polynomials over a field

Theorem

Bézout identity and the Euclidean algorithm for polynomials over a field

Theorem

Every irreducible polynomial over a field is prime

Lemma

Every nonzero nonunit polynomial over a field factors into irreducible polynomials

Theorem

For every field F, F[x] is a unique factorisation domain

Theorem

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

Theorem

A nonzero polynomial of degree n over an integral domain has at most n distinct roots

Corollary

Every finite subgroup of the unit group of an integral domain is cyclic

Corollary

Over an infinite integral domain, equal polynomial functions come from equal polynomials

Theorem

A polynomial of degree two or three over a field is irreducible exactly when it has no root in the field

Definition

The formal derivative of a polynomial

Proposition

Linearity, power rule, Leibniz rule and the degree bound for the formal derivative

Definition

Repeated roots in extension fields and separable polynomials

Theorem

A root is repeated exactly when it is also a root of the formal derivative

Lemma

The monic gcd of two base-field polynomials is unchanged after extending the coefficient field

Theorem

A nonzero polynomial over a field is separable exactly when its gcd with its derivative is 1

Corollary

An irreducible polynomial over a field is separable exactly when its derivative is nonzero

Definition

Content and primitive integer polynomials

Lemma

Content is the positive common divisor of the coefficients divisible by every common divisor

Lemma

The product of primitive integer polynomials is primitive, and contents multiply

Theorem

Gauss lemma: primitive factorisations over ℚ can be cleared to primitive factorisations over ℤ

Theorem

Rational root theorem

Theorem

Irreducibility after reduction modulo a prime implies irreducibility over ℚ when the leading coefficient survives

Theorem

Eisenstein criterion over the integers

Corollary

For every prime p and positive n, xⁿ-p is irreducible over ℚ

Remark

Formal polynomials are not the functions they induce

Sources