PropositionStatement: Literature-sourcedProof: 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.

Linearity, power rule, Leibniz rule and the degree bound for the formal derivative

Statement

For a commutative ring $R$ , polynomials $f, g \in R [x]$ , and $c \in R$ :

$(f + g)^{'} = f^{'} + g^{'}$ and $(c f)^{'} = c f^{'}$ ;
$(x^{n})^{'} = n x^{n - 1}$ for every positive $n$ , while every constant has derivative $0$ ;
$(f g)^{'} = f^{'} g + f g^{'}$ ;
if $f^{'}$ is nonzero, then $\deg f^{'} \leq \deg f - 1$ .

Facts & Assumptions

Given: A commutative ring $R$ and polynomials $f = \sum_{i} a_{i} x^{i}$ and $g = \sum_{j} b_{j} x^{j}$ .

[L1]

The coefficient of $x^{n}$ in $f^{'}$ is $(n + 1) a_{n + 1}$ (The formal derivative of a polynomial).

[L2]

Finite sums may be split, reindexed, and summed in either order over finite products (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

Proof

technique · direct

1.1

Comparing the coefficient at each index in [L1] proves additivity and scalar linearity; applying [L1] to a monomial gives the power rule, including derivative $0$ for constants.

givenL1algebra

1.2

The coefficient of $x^{n}$ in $(f g)^{'}$ is $(n + 1) \sum_{i + j = n + 1} a_{i} b_{j} = \sum_{r + s = n} ((r + 1) a_{r + 1} b_{s} + a_{r} (s + 1) b_{s + 1})$ , where [L2] reindexes the two finite sums; these are exactly the coefficients of $f^{'} g + f g^{'}$ .

givenL1L2algebra

2.1

If $f$ has degree $d$ and $f^{'} \neq 0$ , then [L1] makes every coefficient of $f^{'}$ above index $d - 1$ zero, so $\deg f^{'} \leq d - 1$ ; steps 1.1 and 1.2 establish all remaining claims.

step 1.1step 1.2L1∎

Depends on

Used by

Cited to discharge well-definedness by The formal derivative of a polynomial.

Dependency tree · two levels

8 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

Brian Conrad, Differential Criterion and Primitivity, Section 1 (standard reference, not scraped)