Alphabeta Math
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[x1,…,xn] is an integral domain for every n∈N, including n=0.

Facts & Assumptions

Given: An integral domain R and the iterated polynomial rings P0=R and Pn+1=Pn[xn+1].

[L1]

The iterated ring satisfies R[x1,…,x0]=R and R[x1,…,xn+1]=R[x1,…,xn][xn+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.1basegivenL1

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

1.2ihgiven

Fix n∈N and assume that Pn is a domain.

2.1step 1.1step 1.2L1L2L3discharge-induction∎

Under that hypothesis, [L1] and [L2] make Pn+1=Pn[xn+1] a domain; together with the base case, [L3] proves the claim for every n.

Depends on

Dependency tree · 2 levels

Sources