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.
Over an integral domain, degrees add under multiplication of nonzero polynomials
Statement
If is an integral domain and are nonzero, then and
Facts & Assumptions
Given: An integral domain and nonzero polynomials .
The coefficient of degree in is the product of the two leading coefficients, and all higher coefficients vanish (Degree inequalities for sums and products over a commutative ring).
In an integral domain, a product of two nonzero elements is nonzero (Zero divisor, and integral domain: a commutative ring with and no zero divisors).
Proof
The leading coefficients of and are nonzero, so [L2] makes their product nonzero.
Fact [L1] identifies that product as the coefficient at degree and makes every higher coefficient zero, so , its degree is the sum of the degrees, and its leading coefficient is the product of the leading coefficients.
Depends on
Used by
- A polynomial ring over an integral domain is an integral domain Corollary
- Every finite family of nonzero polynomials has a splitting field, obtained from their product Corollary
- The units of R[x] over an integral domain are exactly the constant polynomials whose values are units of R Corollary
- A polynomial PID has a nonzero Kunneth Tor class Example
- The four roots of t⁴+t+1 over F₂ are the Frobenius powers of any one of them Example
- The rational function field ℝ(t) ordered by the eventual sign is an ordered field, worked out Example
- Every nonzero nonunit polynomial over a field factors into irreducible polynomials Lemma
- Kronecker's one-root step: adjoining a root removes a linear factor and lowers the remaining degree Lemma
- ∑_d∣ nd N_q(d)=qⁿ for the counts N_q(d) of monic irreducibles of degree d over F_q Proposition
- A degree-n polynomial has a splitting field spanned over F by at most n! explicit root monomials Theorem
- A nonzero polynomial of degree n over an integral domain has at most n distinct roots Theorem
- A polynomial of degree two or three over a field is irreducible exactly when it has no root in the field Theorem
- C(x) is not a rational formal power series, so (Cₙ) satisfies no eventual constant-coefficient linear recurrence Theorem
- Division algorithm for polynomials over a field Theorem
- For gcd(n,q)=1 the reduction of Φₙ in F_q[t] is a product of distinct monic irreducibles, each of degree the order of [q] modulo n Theorem
- The recursion defines a unique monic Φₙ∈ℤ[t], of degree φ(n) Theorem
Dependency tree · two levels
7 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)
- Neil Donaldson, Math 120B Notes, Theorem 22.3 (standard reference, not scraped)