set F = FAdj (F_Rat,{2-CRoot(2),zeta});
set K = FAdj (F_Rat,{2-CRoot(2)});
A:
X^2-2 = MinPoly (2-CRoot(2),F_Rat)
by mp, mmv;
FAdj (F_Rat,{2-CRoot(2),zeta}) =
FAdj (F_Rat,({2-CRoot(2)} \/ {zeta}))
by ENUMSET1:1
.=
FAdj ((FAdj (F_Rat,{2-CRoot(2)})),{zeta})
by FIELD_7:35
;
hence deg ((FAdj (F_Rat,{2-CRoot(2),zeta})),F_Rat) =
(deg ((FAdj (F_Rat,{2-CRoot(2),zeta})),(FAdj (F_Rat,{2-CRoot(2)})))) * (deg ((FAdj (F_Rat,{2-CRoot(2)})),F_Rat))
by FIELD_7:30
.=
2 * 2
by A, LL, FIELD_6:67, mmmza
.=
4
;
verum