Alphabeta MathHow 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 over an integral domain is an integral domain
Statement
If is an integral domain, then is an integral domain.
Facts & Assumptions
Given: An integral domain .
Polynomial convolution makes a commutative ring and embeds injectively as the constant polynomials (Polynomial convolution makes a commutative ring containing as its constant subring).
The product of two nonzero polynomials over a domain is nonzero (Over an integral domain, degrees add under multiplication of nonzero polynomials).
An integral domain is a commutative ring with distinct zero and one and no zero divisors (Zero divisor, and integral domain: a commutative ring with and no zero divisors).
Proof
By [L1], is a commutative ring and its zero and one are distinct because the constant embedding is injective.
By [L2], two nonzero polynomials have nonzero product, so [L3] applied with step 1.1 makes an integral domain.
Depends on
Used by
- A polynomial ring in finitely many indeterminates over an integral domain is an integral domain Corollary
- For every field F, F[x] is a Euclidean domain with degree as Euclidean function Corollary
- The product of primitive integer polynomials is primitive, and contents multiply Lemma
- For every field F, F[x] is a unique factorisation domain Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 27 results over 13 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
- Thomas W. Judson, Abstract Algebra: Theory and Applications, Theorem 17.4 (standard reference, not scraped)