[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