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. https://www.cs.ru.nl/~freek/100/ 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? :) Manuel 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 https://www.isa-afp.org/entries/Formal_Puiseux_Series.html > > Many thanks, Manuel! > > Larry > > >
Attachment:
smime.p7s
Description: S/MIME Cryptographic Signature