PropositionStatement: AI-adaptedProof: AI-adaptedprecheck 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.

Finitely supported coefficient sequences and trimmed finite coefficient lists define the same formal polynomials

Statement

Finitely supported coefficient sequences and finite coefficient lists with trailing zeros removed describe the same formal polynomials. Under this correspondence, coefficientwise addition, convolution multiplication, degree, leading coefficient, constants, and the indeterminate agree.

Facts & Assumptions

Given: A commutative ring $R$ , the sequence model $R [x]$ , and the convention that the zero list is the one-term list $(0)$ while every nonzero trimmed list ends in a nonzero coefficient.

[L1]

A polynomial over $R$ is a finitely supported sequence, with coefficientwise addition and convolution multiplication (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L2]

A nonzero polynomial has degree equal to the largest index of a nonzero coefficient and leading coefficient equal to the coefficient at that index; the zero polynomial has neither (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

Proof

technique · direct

1.1

Send a nonzero sequence $a$ to $(a_{0}, \dots, a_{\deg a})$ , send the zero sequence to $(0)$ , and send a trimmed list $(c_{0}, \dots, c_{n})$ to the sequence equal to $c_{i}$ for $i \leq n$ and zero for $i > n$ ; [L2] shows that each construction lands in the stated class and that the two maps are inverse.

givenL1L2construct

2.1

Padding a trimmed list by zeros does not change any coefficient, so the inverse maps preserve coefficientwise sums and every convolution coefficient; [L2] then gives preservation of degree and leading coefficient, and the displayed constant and indeterminate sequences correspond to their usual one-term and two-term lists.

step 1.1L1L2algebra∎

Depends on

Used by

Dependency tree · two levels

4 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

Neil Donaldson, Math 120B Notes, Section 22 (standard reference, not scraped)