In this file we define an operation
derivative (formal differentiation)
on the ring of formal power series in one variable (over an arbitrary commutative semiring).
Under suitable assumptions, we prove that two power series are equal if their derivatives are equal and their constant terms are equal. This will give us a simple tool for proving power series identities. For example, one can easily prove the power series identity $\exp ( \log (1+X)) = 1+X$ by differentiating twice.
Main Definition #
The formal derivative of a power series in one variable.
This is defined here as a function, but will be packaged as a
g have the same constant term and derivative, then they are equal.