CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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.1L1given

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

1.2L2L3given

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$ .

2.1L4step 1.2

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

3.1L5step 2.1algebra

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.

4.1step 1.1step 3.1∎

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

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.

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

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