[isabelle] Prooving the existence of a splitting field
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"
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
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?
and a happy new year :-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and