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 a field F, F(t)=Frac(F[t]) is its rational function field; in particular ℝ(t)=Frac(ℝ[t]) Corollary
- For every field F, F[x] is a Euclidean domain with degree as Euclidean function Corollary
- Tensoring the injection k[x] →(· x) k[x] with k[x]/(x) gives the zero map Example
- Φ₁ through Φ₁₂ computed from the divisor recursion Example
- FALSE: every finitely generated module over a domain is a direct sum of cyclic modules False statement
- If p is a prime not dividing n, a rational minimal polynomial of a primitive n-th root of unity also kills its p-th power Lemma
- The product of primitive integer polynomials is primitive, and contents multiply Lemma
- ∑_d∣ nd N_q(d)=qⁿ for the counts N_q(d) of monic irreducibles of degree d over F_q Proposition
- Φ_pʳ(t)=∑_k<pt^kpʳ⁻¹, and Φ_pʳ(t+1) is Eisenstein at p Proposition
- For every field F, F[x] is a unique factorisation domain Theorem
- Over a field whose characteristic does not divide n, the roots of Φₙ are exactly the primitive roots of unity Theorem
- The recursion defines a unique monic Φₙ∈ℤ[t], of degree φ(n) Theorem
Dependency tree · two levels
11 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
- Thomas W. Judson, Abstract Algebra: Theory and Applications, Theorem 17.4 (standard reference, not scraped)