Re: [isabelle] Algebraically closed fields



Dear Manuel,

thanks for your useful answer.

> It is not necessarily bad to introduce a typeclass that has only one
> instance – especially when it coincides with a standard mathematical
> concept (as is the case here). However, it also doesn't have much
> immediate payoff, which is probably why no one has done it so far. Feel
> free to do so!

I will do so; should be no problem.

>
> There is also a HOL-Algebra development by former students of
> Larry/Anthony (much of it still in a private repository) that could be
> used to make a generic "alg_closure" type constructor. Not sure how
> useful that is though – it might be interesting when reasoning about
> things like Galois fields or also for generic proofs involving fields,
> because it allows you to suddenly go to the algebraic closure for a
> proof and then back.

I was also thinking of something like that, although this does not have
immediate priority for me. Actually, I only want to have algebraically
closed fields for formalizing Hilbert's Nullstellensatz in the most
general setting (i.e. not restricted to complex numbers), which I'm
working on right now.

Best regards,
Alexander


>
> Another interesting instance would be formal Puiseux series. They've
> been on my long-term potential to-do list. If anyone feels like having a
> go at them (e.g. in analogy to the existing formal power series/Laurent
> series in HOL-Compuational_Algebra), please do. :)
>
> Cheers,
>
> Manuel
>
>
> On 08/04/2019 16:18, Alexander Maletzky wrote:
>> Dear list,
>>
>> is there some type class of algebraically closed fields in Isabelle/HOL?
>> Since such fields are an important and widely used concept I'd be
>> surprised if not, but a quick search in the library+AFP did not reveal
>> anything ...
>>
>> Of course I could easily introduce a suitable type class myself, but I
>> just wanted to avoid duplicate work.
>>
>> Best regards,
>> Alexander
>>
>>
>>
>





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