Immediate from the definition by reindexing \(n \mapsto n+1\).

By definition.

Follows directly from the definition of the derivative.

All coefficients of \(0\) are \(0\), so the derivative is \(0\).

\(1\) is constant, so \(1^{\prime } = 0\).

All coefficients of \(c\) beyond the constant term are \(0\), so the derivative is \(0\).

The \(0\)-th coefficient of \(x^{\prime }\) is \((0+1) \cdot [x^1]x = 1\), and all higher coefficients are \(0\).

Direct coefficient comparison: \([x^m](x^{n+1})^{\prime } = (m+1) \cdot [x^{m+1}](x^{n+1})\). This is \((n+1)\) if \(m = n\) and \(0\) otherwise.

Write \(n = m + 1\) and apply Lemma 1.192.

Both derivatives are defined by the same coefficient formula.

This combines parts (a) through (h), proved individually below.

This is part of [ 19s-mt3s , Exercise 5 (b) ] (specifically, it is Statement 1 in [ 19s-mt3s , solution to Exercise 5 (b) ] ).

The derivative is an additive map, so it preserves negation.

The derivative is an additive map, so it preserves subtraction.

Follows from additivity (part (a)) by induction on \(|I|\).

For each coefficient index \(n\), the set of \(i\) with \([x^n]f_i^{\prime } \neq 0\) is a subset of the set of \(i\) with \([x^{n+1}]f_i \neq 0\), which is finite by summability of \((f_i)\).

This is the natural generalization of Theorem 1.195 (a) to (potentially) infinite sums. The proof works coefficient-by-coefficient: for each \(n\),

where the interchange of summation and multiplication by \((n+1)\) is justified because the sum has finite support.

This is part of [ 19s-mt3s , Exercise 5 (b) ] (specifically, it is Statement 3 in [ 19s-mt3s , solution to Exercise 5 (b) ] ).

This follows from the scalar multiplication rule (Lemma 1.202), since \(C(c) \cdot f = c \cdot f\) in the power series ring.

This is [ 19s-mt3s , Exercise 5 (c) ] and [ Grinbe17 , Proposition 0.2 (c) ] .

Let \(f,g\in K\left[ \left[ x\right] \right] \) be two FPSs such that \(g\) is invertible. Then, Theorem 1.195 (d) (applied to \(\frac{f}{g}\) instead of \(f\)) yields \(\left( \frac{f}{g}\cdot g\right) ^{\prime }=\left( \frac{f}{g}\right) ^{\prime }\cdot g+\frac{f}{g}\cdot g^{\prime }\). In view of \(\frac{f}{g}\cdot g=f\), this rewrites as \(f^{\prime }=\left( \frac{f}{g}\right) ^{\prime }\cdot g+\frac{f}{g}\cdot g^{\prime }\). Solving this for \(\left( \frac{f}{g}\right) ^{\prime }\), we find \(\left( \frac{f}{g}\right) ^{\prime }=\frac{f^{\prime }g-fg^{\prime }}{g^{2}}\).

This follows by induction on \(n\), using part (d) (in the induction step) and \(1^{\prime }=0\) (in the induction base).

Let \(f,g\in K\left[ \left[ x\right] \right] \) be two FPSs such that \(f\) is a polynomial or \(\left[ x^{0}\right] g=0\). Write the FPS \(f\) in the form \(f=\sum _{n\in \mathbb {N}}f_{n}x^{n}\) with \(f_{0},f_{1},f_{2},\ldots \in K\). Then, \(f\left[ g\right] =\sum _{n\in \mathbb {N}}f_{n}g^{n}\). Hence,

On the other hand, from \(f=\sum _{n\in \mathbb {N}}f_{n}x^{n}\), we obtain \(f^{\prime }=\sum _{n{\gt}0}nf_{n}x^{n-1}=\sum _{m\in \mathbb {N}}\left( m+1\right) f_{m+1}x^{m}\) (here, we have substituted \(m+1\) for \(n\) in the sum). Hence,

(here, we have substituted \(n-1\) for \(m\) in the sum). Multiplying both sides of this equality by \(g^{\prime }\), we find

Comparing this with (25), we find \(\left( f\left[ g\right] \right) ^{\prime }=f^{\prime }\left[ g\right] \cdot g^{\prime }\). In other words, \(\left( f\circ g\right) ^{\prime }=\left( f^{\prime }\circ g\right) \cdot g^{\prime }\) (since \(f\circ g\) is a synonym for \(f\left[ g\right] \)).

The proof can be found in [ Grinbe17 , Lemma 0.3 ] . Let \(n \geq 1\). From \(f^{\prime } = g^{\prime }\), comparing coefficients at index \(n - 1\) yields \(n \cdot [x^n]f = n \cdot [x^n]g\). Since \(K\) is a \(\mathbb {Q}\)-algebra (hence torsion-free), we can divide by \(n\) to conclude \([x^n]f = [x^n]g\), i.e., \([x^n](f - g) = 0\).

Note that the condition that \(K\) be a \(\mathbb {Q}\)-algebra is crucial, since it allows dividing by positive integers. (For example, if \(K\) could be \(\mathbb {Z}/2\), then we would easily get a counterexample, e.g., by taking \(f=x^{2}\) and \(g=0\).)

By Lemma 1.208, \(f - g\) is constant. Since \([x^0](f - g) = [x^0]f - [x^0]g = 0\), we have \(f - g = 0\), so \(f = g\).