Formal power series (Q5891671)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 6062054
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Formal power series |
scientific article; zbMATH DE number 6062054 |
Statements
Formal power series (English)
0 references
31 July 2012
0 references
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.
0 references
formalization of mathematics
0 references
theorem proving
0 references
formal power series
0 references
generating functions
0 references
\texttt{Isabelle/HOL}
0 references
0.7739402055740356
0 references
0.7696372270584106
0 references
0.7675458192825317
0 references
0.766849160194397
0 references
0.7601003646850586
0 references
