*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Algebraically closed fields*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Mon, 8 Apr 2019 17:52:32 +0200*In-reply-to*: <8bc54c01-d7f1-0e3d-2cfb-ffdb29733f8a@risc.jku.at>*References*: <8bc54c01-d7f1-0e3d-2cfb-ffdb29733f8a@risc.jku.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.5.3

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

**Follow-Ups**:**Re: [isabelle] Algebraically closed fields***From:*Alexander Maletzky

**References**:**[isabelle] Algebraically closed fields***From:*Alexander Maletzky

- Previous by Date: [isabelle] Algebraically closed fields
- Next by Date: Re: [isabelle] Isabelle2019-RC0: generate_file - documentation and behavior
- Previous by Thread: [isabelle] Algebraically closed fields
- Next by Thread: Re: [isabelle] Algebraically closed fields
- Cl-isabelle-users April 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list