# [isabelle] Prooving the existence of a splitting field

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

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