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,

> 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.