let F be Field; :: thesis: for E being Polynom-Ring F -homomorphic FieldExtension of F
for a being F -algebraic Element of E holds (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), FAdj (F,{a}) are_isomorphic
let E be Polynom-Ring F -homomorphic FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), FAdj (F,{a}) are_isomorphic
let a be F -algebraic Element of E; :: thesis: (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), FAdj (F,{a}) are_isomorphic
set f = hom_Ext_eval (a,F);
(Polynom-Ring F) / (ker (hom_Ext_eval (a,F))), Image (hom_Ext_eval (a,F)) are_isomorphic by RING_2:15;
then (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), Image (hom_Ext_eval (a,F)) are_isomorphic by mpol1;
then (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), RAdj (F,{a}) are_isomorphic by lemphi4;
hence (Polynom-Ring F) / ({(MinPoly (a,F))} -Ideal), FAdj (F,{a}) are_isomorphic by ch1; :: thesis: verum