:: deftheorem psi defines Psi FIELD_8:def 10 :
for F1 being Field
for F2 being b₁ -homomorphic b₁ -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
for b₉ being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) holds
( b₉ = Psi (a,b,h,p) iff for r being Element of the carrier of (Polynom-Ring F1) holds b₉ . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) );