Formal power series (Q5891671)

This paper presents a formalization of the topological ring of formal power series in \texttt{Isabelle/HOL}. The following constructions are formalized: division, the formal derivative, various basic manipulations on formal power series (shifting, differentiating, general convolutions and powers), as well as radicals, composition and reverses. As an example, the exponential, binomial and hyper-geometric series are introduced as characterizing all the solutions of a certain formal differential equation. It is shown that this approach yields extremely short proofs for the binomial theorem and Vandermonde's identity. Also, logarithmic and some trigonometric series are defined; it is shown that some of the properties hold without any convergence consideration. Finally, it is shown that, using a generic formalization of the fraction field of an integral domain, Laurent series and rational functions can be obtained for free.