*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Prooving the existence of a splitting field*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 03 Jan 2014 13:29:18 +0100*In-reply-to*: <52C59841.90906@gmx.de>*References*: <52C59841.90906@gmx.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

I don't think field extensions have been formalized in Isabelle before. I suspect you first have to define a new type that is big enough to contain all the extension you will need and then work within that. But that is just a rough guess. Tobias On 02/01/2014 17:48, Markus Schmetkamp wrote: > Hi people, > > I'm trying to prove, that for every univariate polynomial has a splitting field > i.e. a field where the polynomial factors completely into linear factors. At > first it's okay, if this field isn't the smallest field with that property. > I'm using the HOL/Algebra library (and version Isabelle2013-1) and have already > proved several useful lemmas. I defined term "field extension" this way > > locale field_extension = > fixes L::"('a, 'n) ring_scheme" (structure) and K::"('b, 'm) ring_scheme" > and iota::"'b => 'a" > assumes field_L[intro, simp]: "field L" > and field_K[intro, simp]: "field K" > and hom[intro, simp]: "iota ? ring_hom K L" > > furthermore I could prove this theorem > > theorem extension_with_zero: > fixes K::"'b ring" and p > assumes "field K" > and "p ? carrier (UP K)" > and "deg K p ~= 0" > shows "?(L?(nat ? 'b) set ring). ?iota. ?x ? carrier L. field_extension L K ? ? > eval K L iota x p = zero L" > > That shows that you can find a field in which the polynomial has at least one > root. Next you could use long division to reduce the polynomial and repeat the > process until you have a field which contains every root of the polynomial. That > would be a solution... > > Now the problem: > Isabelle forces me to specify the type of the object which existence I want to > show. Unfortunately the field I get from the theorem from above has another > "bigger" type than the field I'm starting with. If you want to repeat the > process you had to know the number of repetitions you make, but that varies with > the polynomial. > > Has anyone an idea or a solution? > > Best wishes > Markus > > and a happy new year :-)

**References**:**[isabelle] Prooving the existence of a splitting field***From:*Markus Schmetkamp

- Previous by Date: [isabelle] Prooving the existence of a splitting field
- Next by Date: [isabelle] Preliminary Cfp ACL2'2014
- Previous by Thread: [isabelle] Prooving the existence of a splitting field
- Next by Thread: [isabelle] Preliminary Cfp ACL2'2014
- Cl-isabelle-users January 2014 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