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



I know, I already compiled a list of those and intend to publish it soon
(as soon as I figure out how to properly do syntax highlighting).

Manuel


On 24/02/2021 17:10, Wenda Li wrote:
> 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
>>>
>>>
>>>
>>
> 

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



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