[isabelle] New in the AFP: Formal Puiseux Series

I am happy to announce another entry from Manuel Eberl, who is one of our most prolific contributors: 

Formal Puiseux series are generalisations of formal power series and formal Laurent series that also allow for fractional exponents. … 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.

You will find it online at https://www.isa-afp.org/entries/Formal_Puiseux_Series.html

Many thanks, Manuel!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.