Re: [isabelle] Algebraically closed fields

Dear Alexander,

having a type-class for alg.-closed fields would definitely be something nice.
For instance, then one can also generalize the existence of a Jordan-Normal-Form
to alg.-closed fields.

Moreover, I hope in the long run that there will be at least to instances:
complex numbers and complex algebraic numbers.


> Am 09.04.2019 um 09:00 schrieb Alexander Maletzky <alexander.maletzky at>:
> 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

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