Formal Puiseux Series

 

Title: Formal Puiseux Series
Author: Manuel Eberl
Submission date: 2021-02-17
Abstract:

Formal Puiseux series are generalisations of formal power series and formal Laurent series that also allow for fractional exponents. They have the following general form: \[\sum_{i=N}^\infty a_{i/d} X^{i/d}\] where N is an integer and d is a positive integer.

This entry defines these series including their basic algebraic properties. Furthermore, it proves the Newton–Puiseux Theorem, namely that the Puiseux series over an algebraically closed field of characteristic 0 are also algebraically closed.

BibTeX:
@article{Formal_Puiseux_Series-AFP,
  author  = {Manuel Eberl},
  title   = {Formal Puiseux Series},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Formal_Puiseux_Series.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Polynomial_Interpolation
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.