CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-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.

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

Statement

If $R$ is an integral domain, then $R[x_1,\ldots,x_n]$ is an integral domain for every $n\in\mathbb N$ , including $n=0$ .

Facts & Assumptions

Given: An integral domain $R$ and the iterated polynomial rings $P_0=R$ and $P_{n+1}=P_n[x_{n+1}]$ .

[L1]

The iterated ring satisfies $R[x_1,\ldots,x_0]=R$ and $R[x_1,\ldots,x_{n+1}]=R[x_1,\ldots,x_n][x_{n+1}]$ (Polynomial rings in finitely many commuting indeterminates by iteration).

[L2]

A one-variable polynomial ring over an integral domain is an integral domain (A polynomial ring over an integral domain is an integral domain).

[L3]

If a property holds at $0$ and passes from $n$ to $n+1$ , it holds for every natural number (The principle of mathematical induction).

Proof

technique · induction

1.1

The ring $P_0=R$ is a domain, giving the zero-indeterminate case.

basegivenL1

1.2

Fix $n\in\mathbb N$ and assume that $P_n$ is a domain.

ihgiven

2.1

Under that hypothesis, [L1] and [L2] make $P_{n+1}=P_n[x_{n+1}]$ a domain; together with the base case, [L3] proves the claim for every $n$ .

step 1.1step 1.2L1L2L3discharge-induction∎

Depends on

Used by

For a field F, the ideal (x,y) in F[x,y] is not principal Counterexample

Dependency tree · next 3 levels

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

Neil Donaldson, Math 120B Notes, Section 22, More general constructions (standard reference, not scraped)