CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

$R [x]$ is Noetherian if and only if $R$ is Noetherian

Statement

Let $R$ be a commutative ring. Then $R [x]$ is Noetherian if and only if $R$ is Noetherian.

Facts & Assumptions

Given: A commutative ring $R$ and its polynomial ring $R [x]$ .

[L1]

If $R$ is a Noetherian commutative ring then $R [x]$ is a Noetherian commutative ring (Hilbert basis theorem: if $R$ is Noetherian then $R [x]$ is Noetherian).

[L2]

For commutative rings $R, S$ , a unital ring homomorphism $φ ⁣ : R \to S$ and $s \in S$ , there is a unique unital ring homomorphism ${ev}_{φ, s} ⁣ : R [x] \to S$ that extends $φ$ on constant polynomials and sends $x$ to $s$ (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[L3]

For a unital ring homomorphism $φ ⁣ : R \to S$ between commutative rings, $s \in S$ and $f = \sum_{i} a_{i} x^{i} \in R [x]$ , the value of $f$ at $s$ along $φ$ is $f_{φ} (s) = \sum_{i} φ (a_{i}) s^{i}$ (Evaluation and roots of a polynomial in a commutative target ring).

[L4]

For a ring homomorphism $f ⁣ : R \to S$ there is a ring isomorphism $R / \ker f ≅ im f$ (First isomorphism theorem for rings: $R / \ker f ≅ im f$ ).

[L5]

Every quotient $R / I$ of a Noetherian commutative ring by an ideal is Noetherian (Every quotient and every localisation of a Noetherian ring is Noetherian).

Proof

technique · direct

1.1

For the direction from $R$ to $R [x]$ , the Hilbert basis theorem applied to $R$ gives at once that $R [x]$ is Noetherian.

L1given

1.2

For the converse direction, take $φ$ to be the identity of $R$ and $s = 0_{R}$ in the universal property: there is a unital ring homomorphism $ε ⁣ : R [x] \to R$ , evaluation at $0$ , which is the identity on constant polynomials and sends $x$ to $0$ . Being the identity on constants makes $ε$ surjective, so $im ε = R$ .

L2L3given

2.1

Still for the converse direction, the first isomorphism theorem applied to $ε$ gives a ring isomorphism $R [x] / \ker ε ≅ R$ .

L4step 1.2

3.1

Still for the converse direction, assume $R [x]$ Noetherian. Its quotient $R [x] / \ker ε$ is then Noetherian, and a ring isomorphism carries ideals to ideals and finite generating lists to finite generating lists, so the isomorphic ring $R$ is Noetherian.

L5step 2.1algebra

4.1

Step 1.1 is one implication and step 3.1 is the other, so $R [x]$ is Noetherian exactly when $R$ is.

step 1.1step 3.1∎

Remarks

Which half is the theorem. The direction from $R$ to $R [x]$ is the Hilbert basis theorem and carries all the work; the converse is three citations, since $R$ is a quotient of $R [x]$ and quotients of Noetherian rings are Noetherian.
Evaluation at any element of $R$ would do. The argument uses only that $ε$ is a surjective ring homomorphism $R [x] \to R$ ; evaluation at $0$ is chosen because it is the one whose kernel, the ideal of polynomials with zero constant term, is the easiest to name.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise (16.8) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, §3 (standard reference, not scraped)

R[x]R[x] is Noetherian if and only if RR is Noetherian