Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck 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.

Over an integral domain, degrees add under multiplication of nonzero polynomials

Statement

If RR is an integral domain and f,g∈R[x]f,g\in R[x] are nonzero, then fg≠0fg\ne0 and

deg⁡(fg)=deg⁡f+deg⁡g,lc⁡(fg)=lc⁡(f)lc⁡(g).\deg(fg)=\deg f+\deg g,\qquad \operatorname{lc}(fg)=\operatorname{lc}(f)\operatorname{lc}(g).

Facts & Assumptions

Given: An integral domain RR and nonzero polynomials f,g∈R[x]f,g\in R[x].

[L1]

The coefficient of degree deg⁡f+deg⁡g\deg f+\deg g in fgfg is the product of the two leading coefficients, and all higher coefficients vanish (Degree inequalities for sums and products over a commutative ring).

[L2]

In an integral domain, a product of two nonzero elements is nonzero (Zero divisor, and integral domain: a commutative ring with 1≠01 \ne 0 and no zero divisors).

Proof

technique · direct
1.1

The leading coefficients of ff and gg are nonzero, so [L2] makes their product nonzero.

givenL2
2.1

Fact [L1] identifies that product as the coefficient at degree deg⁡f+deg⁡g\deg f+\deg g and makes every higher coefficient zero, so fg≠0fg\ne0, its degree is the sum of the degrees, and its leading coefficient is the product of the leading coefficients.

step 1.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

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