TheoremStatement: 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.

Substitution by a zero-constant series is a ring homomorphism, and composition is associative when both inner series have zero constant coefficient

Statement

Let $g \in R ⟦ x ⟧$ have zero constant coefficient. Then

$S_{g} : R ⟦ x ⟧ \to R ⟦ x ⟧, S_{g} (f) = f \circ g,$

is a unital ring homomorphism. Thus

$(f + h) \circ g = f \circ g + h \circ g, (f h) \circ g = (f \circ g) (h \circ g), 1 \circ g = 1.$

If $g$ and $h$ both have zero constant coefficient, then

$(f \circ g) \circ h = f \circ (g \circ h)$

for every $f \in R ⟦ x ⟧$ . Admissibility of the four displayed compositions is not by itself enough for this identity; the hypothesis on the two inner series is what makes both sides the same locally finite rearrangement.

Also $f \circ x = f$ and $x \circ f = f$ . Composition need not be commutative.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

Formal composition is $f \circ g = \sum_{n \geq 0} [x^{n}] f g^{n}$ , defined when $f$ is a polynomial or when $g (0) = 0$ (Composition $f \circ g$ of formal series when the outer series is a polynomial or the inner series has zero constant term).

[F2]

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).

[F3]

Multiplication by a fixed formal series distributes over a summable family (Summable formal families may be regrouped and rearranged, distribute over multiplication, and have well-defined locally finite products).

Proof

technique · compare finite coefficient sums

1.1

Linearity follows by splitting the locally finite defining sum. For multiplication, expand $(f h) \circ g$ using the Cauchy coefficients of $f h$ and regroup the locally finite double family to obtain $(\sum_{i} [x^{i}] f g^{i}) (\sum_{j} [x^{j}] h g^{j})$ . Constants give $1 \circ g = 1$ .

givenF1F2F3

1.2

For associativity assume $[x^{0}] g = [x^{0}] h = 0$ . Then ${ord}_{x} (g^{n}) \geq n$ and ${ord}_{x} (h^{m}) \geq m$ , so expanding either side by [F1] gives the same doubly indexed family $[x^{n}] f [x^{m}] (g^{n}) h^{m}$ , in which only finitely many terms contribute below each degree. [F2] therefore rearranges one into the other. The hypothesis is used exactly here: without it a term of arbitrarily high index can contribute in low degree, and the two sides need not agree even when all four compositions are individually admissible.

givenF1F2

1.3

Substituting $x$ leaves every coefficient in place, while substituting into the polynomial $x$ returns the inner series. Finally, $x^{2} \circ (x + x^{2}) = x^{2} + 2 x^{3} + x^{4}$ whereas $(x + x^{2}) \circ x^{2} = x^{2} + x^{4}$ over $Z$ , so composition is not commutative.

givenF1

2.1

Steps 1.1-1.3 give the homomorphism, associativity, identity, and noncommutativity claims.

step 1.1step 1.2step 1.3∎

Depends on

Used by

Dependency tree · two levels

10 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)