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.

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



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