CorollaryStatement: 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.

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

Statement

Let $R$ be an integral domain. A polynomial $f\in R[x]$ is a unit if and only if it is a constant polynomial whose constant value is a unit of $R$ .

Facts & Assumptions

Given: An integral domain $R$ and a polynomial $f\in R[x]$ .

[L1]

For nonzero polynomials over a domain, $\deg(fg)=\deg f+\deg g$ (Over an integral domain, degrees add under multiplication of nonzero polynomials).

[L2]

The constant-polynomial map is an injective unital ring homomorphism $R\to R[x]$ (Polynomial convolution makes $R[x]$ a commutative ring containing $R$ as its constant subring).

Proof

technique · direct

1.1

If $f$ is a unit, choose $g$ with $fg=1$ ; neither factor is zero and [L1] gives $0=\deg1=\deg f+\deg g$ , so both degrees are $0$ , and comparison of constant coefficients shows that the constant value of $f$ is a unit of $R$ .

givenL1L2choose

2.1

Conversely, if $u\in R$ is a unit with inverse $v$ , then [L2] gives $c(u)c(v)=c(uv)=c(1)=1$ , so the constant polynomial $u$ is a unit of $R[x]$ .

L2algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 20 results over 8 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

James McKernan, MIT 18.703 Lecture 21, Lemma 21.1 (standard reference, not scraped)

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