CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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}, \dots, x_{n}]$ is an integral domain for every $n \in 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}, \dots, x_{0}] = R$ and $R [x_{1}, \dots, x_{n + 1}] = R [x_{1}, \dots, 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 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

Dependency tree · two levels

10 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

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