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



In fact, many of the ’newer’ theorems that appears at the bottom of Freek’s website but don’t count as the 100 theorems are also available in Isabelle. We may ask Freek for a longer list :-)

Wenda

> On 24 Feb 2021, at 14:59, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> 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
>> 
>> 
>> 
> 





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