Re: [isabelle] Algebraically closed fields



I don't think there is. As far as I know, the visible Isabelle universe
only contains two concrete instances of algebraically closed fields,
namely the complex numbers (in HOL) and the algebraic complex numbers
(in the AFP entry Algebraic_Numbers). The latter are, I think, more
technically interesting and not so much for abstract mathematical
developments.

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!

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.

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.