Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-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.

Degree inequalities for sums and products over a commutative ring

Statement

Let RR be a commutative ring and let f,g∈R[x]f,g\in R[x] be nonzero.

  1. If f+g≠0f+g\ne0, then deg⁡(f+g)≤max⁡{deg⁡f,deg⁡g}\deg(f+g)\le\max\{\deg f,\deg g\}.
  2. The coefficient of xdeg⁡f+deg⁡gx^{\deg f+\deg g} in fgfg is lc⁡(f)lc⁡(g)\operatorname{lc}(f)\operatorname{lc}(g). If fg≠0fg\ne0, then deg⁡(fg)≤deg⁡f+deg⁡g\deg(fg)\le\deg f+\deg g.

Facts & Assumptions

Given: Nonzero polynomials f=∑iaixif=\sum_i a_i x^i and g=∑jbjxjg=\sum_j b_jx^j over a commutative ring RR.

[L1]

Degree is the greatest index with nonzero coefficient, and the coefficient there is the leading coefficient (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L2]

Polynomial addition is coefficientwise and the coefficient of xkx^k in a product is ∑i+j=kaibj\sum_{i+j=k}a_i b_j (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

Proof

technique · direct
1.1

For every k>max⁡{deg⁡f,deg⁡g}k>\max\{\deg f,\deg g\} both aka_k and bkb_k vanish, so the coefficient of xkx^k in f+gf+g vanishes; if the sum is nonzero, [L1] gives the stated inequality.

givenL1L2
2.1

Put m=deg⁡fm=\deg f and n=deg⁡gn=\deg g. For k>m+nk>m+n, every pair i+j=ki+j=k has i>mi>m or j>nj>n, while for k=m+nk=m+n the only possibly nonzero summand is ambna_m b_n; hence the top displayed coefficient is lc⁡(f)lc⁡(g)\operatorname{lc}(f)\operatorname{lc}(g) and any nonzero product has degree at most m+nm+n.

givenL1L2algebra∎

Depends on

Used by

Dependency tree · next 3 levels

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