let F be ordered Field; :: thesis: for P being Ordering of F
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for a being Element of E st deg p is odd & a is_a_root_of p,E holds
P extends_to FAdj (F,{a})
let P be Ordering of F; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for a being Element of E st deg p is odd & a is_a_root_of p,E holds
P extends_to FAdj (F,{a})
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for E being FieldExtension of F
for a being Element of E st deg p is odd & a is_a_root_of p,E holds
P extends_to FAdj (F,{a})
let E be FieldExtension of F; :: thesis: for a being Element of E st deg p is odd & a is_a_root_of p,E holds
P extends_to FAdj (F,{a})
let a be Element of E; :: thesis: ( deg p is odd & a is_a_root_of p,E implies P extends_to FAdj (F,{a}) )
H: deg (NormPolynomial p) = deg p by lemdeg;
assume AS: ( deg p is odd & a is_a_root_of p,E ) ; :: thesis: P extends_to FAdj (F,{a})
then A: Ext_eval (p,a) = 0. E by FIELD_4:def 2;
then reconsider a = a as F -algebraic Element of E by FIELD_6:43;
MinPoly (a,F) = NormPolynomial p by A, FIELD_8:15;
then deg ((FAdj (F,{a})),F) = deg (NormPolynomial p) by FIELD_6:67;
hence P extends_to FAdj (F,{a}) by AS, H, main; :: thesis: verum