let F be Field; for E being FieldExtension of F
for a being Element of E holds
( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )
let E be FieldExtension of F; for a being Element of E holds
( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )
let a be Element of E; ( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )
reconsider E1 = E as Polynom-Ring F -homomorphic Field ;
reconsider g = hom_Ext_eval (a,F) as Homomorphism of (Polynom-Ring F),E1 ;
H:
(Polynom-Ring F) / (ker g), Image g are_isomorphic
by RING_2:15;
hence
( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )
by A; verum