let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E holds deg ((FAdj (F,{a})),F) = deg (MinPoly (a,F))
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds deg ((FAdj (F,{a})),F) = deg (MinPoly (a,F))
let a be F -algebraic Element of E; :: thesis: deg ((FAdj (F,{a})),F) = deg (MinPoly (a,F))
set B = Base a;
set m = deg (MinPoly (a,F));
B: card (Base a) = deg (MinPoly (a,F)) by lembascard;
C: Base a is Basis of (VecSp ((FAdj (F,{a})),F)) by lembas;
then A: VecSp ((FAdj (F,{a})),F) is finite-dimensional by MATRLIN:def 1;
then dim (VecSp ((FAdj (F,{a})),F)) = deg (MinPoly (a,F)) by C, B, VECTSP_9:def 1;
hence deg ((FAdj (F,{a})),F) = deg (MinPoly (a,F)) by A, FIELD_4:def 7; :: thesis: verum