PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

Formal differentiation is linear and satisfies product, power, quotient, chain, and coefficient-recovery laws

Statement

For formal series over a commutative ring,

$D (f + g) = D f + D g, D (r f) = r D f, D (f g) = (D f) g + f D g,$

and, for $m \in N$ ,

$D (f^{m}) = m f^{m - 1} D f$

when $m \geq 1$ , while $D (f^{0}) = D (1) = 0$ . If $f$ is a unit, then

$D (f^{- 1}) = - f^{- 2} D f .$

Consequently, if $g$ is a unit, then

$D (f / g) = \frac{(D f) g - f D g}{g^{2}} .$

Whenever $f \circ g$ is admissible and the resulting termwise differentiated family is summable,

$D (f \circ g) = (D f \circ g) D g .$

If $R$ is a commutative $Q$ -algebra, then $[x^{n}] f = (D^{n} f) (0) / n!$ . Over any commutative ring the Hasse derivative

$D^{[n]} f : = \sum_{m \geq n} (\binom{m}{n}) [x^{m}] f x^{m - n}$

satisfies $(D^{[n]} f) (0) = [x^{n}] f$ . Finally, if $f (0) = g (0) = 0$ and $g^{'} (0)$ is a unit, then $f / g$ is a well-defined formal series and

$[x^{0}] (f / g) = f^{'} (0) g^{'} (0)^{- 1} .$

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

The formal derivative of $\sum_{n \geq 0} a_{n} x^{n}$ is $\sum_{n \geq 1} n a_{n} x^{n - 1}$ (The formal derivative $D (\sum a_{n} x^{n}) = \sum_{n \geq 1} n a_{n} x^{n - 1}$ ).

[F2]

For every natural number $n$ , $(\binom{n}{n}) = 1$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[F3]

Multiplication by $x^{k}$ shifts coefficients: $[x^{n}] (x^{k} f) = [x^{n - k}] f$ for $k \leq n$ and is $0$ for $k > n$ (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[F4]

A formal power series is a unit exactly when its constant coefficient is a unit (A formal power series is a unit exactly when its constant coefficient is a unit).

[F5]

A summable family may be bijectively reindexed or partitioned and regrouped without changing its sum (Summable formal families may be regrouped and rearranged, distribute over multiplication, and have well-defined locally finite products).

Proof

technique · coefficient comparison

1.1

Linearity is immediate coefficientwise. In degree $n - 1$ , $D (f g)$ has coefficient $n \sum_{i + j = n} a_{i} b_{j}$ , while $(D f) g + f D g$ has $\sum_{i + j = n} (i + j) a_{i} b_{j}$ ; these are equal. Induction on $m$ gives the power rule, including the separately stated $m = 0$ case.

givenF1

1.2

Iterating the derivative gives $(D^{n} f) (0) = n! [x^{n}] f$ ; in a $Q$ -algebra $n!$ is invertible, proving ordinary recovery. The constant coefficient of $D^{[n]} f$ is the $m = n$ term $(\binom{n}{n}) [x^{n}] f = [x^{n}] f$ , so Hasse recovery needs no division and works in every characteristic.

givenF1F2

1.3

Write $f = x F$ and $g = x G$ using the shift formula. Then $G (0) = g^{'} (0)$ is a unit, so $g = x G$ and $f = x F$ give $f / g = F G^{- 1}$ . Its constant coefficient is $F (0) G (0)^{- 1} = f^{'} (0) g^{'} (0)^{- 1}$ .

givenF3F4

2.1

Differentiating $f f^{- 1} = 1$ and using the product rule gives $(D f) f^{- 1} + f D (f^{- 1}) = 0$ ; multiplying by $f^{- 1}$ gives the inverse rule. Applying the product rule to $f / g = f g^{- 1}$ and then the inverse rule gives $D (f / g) = ((D f) g - f D g) g^{- 2}$ .

step 1.1given

2.2

The chain rule holds for an outer monomial by the power rule. Linearity and locally finite rearrangement extend it to every admissible composition for which the differentiated family is summable.

step 1.1givenF5

3.1

Steps 1.1-2.2 prove every displayed law and its stated hypotheses.

step 1.1step 2.1step 2.2step 1.2step 1.3∎

Depends on

Used by

Dependency tree · two levels

22 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

Benjamin Sambale, An Invitation to Formal Power Series (standard reference, not scraped)
Herbert S. Wilf, generatingfunctionology (standard reference, not scraped)