Re: [isabelle] New in the AFP: Formal Puiseux Series

Please do excuse the frivolous remark, but I cannot resist pointing out
that with this, we are now exactly one theorem behind HOL Light on Freek
Wiedijk's list.

Perhaps someone feels inspired to formalise some more things from there
so that we will finally pull ahead? Some geometry perhaps? Or port
something over from HOL Light?



On 24/02/2021 15:17, Lawrence Paulson wrote:
> 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
> Many thanks, Manuel!
> Larry

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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