Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)audited 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.

Polynomial rings in finitely many commuting indeterminates by iteration

Definition

Let RR be a commutative ring. Define polynomial rings in finitely many commuting indeterminates recursively by

R[x1,…,x0]:=R,R[x1,…,xn+1]:=R[x1,…,xn][xn+1].R[x_1,\ldots,x_0]:=R,\qquad R[x_1,\ldots,x_{n+1}]:=R[x_1,\ldots,x_n][x_{n+1}].

At each stage the coefficient ring embeds as the constant polynomials (Polynomial convolution makes R[x]R[x] a commutative ring containing RR as its constant subring), so all preceding indeterminates remain present. The new indeterminate commutes with every coefficient by the commutativity built into The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, and consequently all xix_i commute. This iterated ring is denoted R[x1,…,xn]R[x_1,\ldots,x_n].

Depends on

Used by

Dependency tree · next 3 levels

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