let F be Field; :: thesis: for E being FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F)
for q being non constant Element of the carrier of (Polynom-Ring E) st p = q holds
( p is separable iff q is separable )
let E be FieldExtension of F; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for q being non constant Element of the carrier of (Polynom-Ring E) st p = q holds
( p is separable iff q is separable )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for q being non constant Element of the carrier of (Polynom-Ring E) st p = q holds
( p is separable iff q is separable )
let q be non constant Element of the carrier of (Polynom-Ring E); :: thesis: ( p = q implies ( p is separable iff q is separable ) )
assume AS: p = q ; :: thesis: ( p is separable iff q is separable )

A: now :: thesis: ( p is separable implies q is separable )

assume p is separable ; :: thesis: q is separable
then B: p gcd ((Deriv F) . p) = 1_. F by Thsepgcd;
(Deriv E) . q = (Deriv F) . p by AS, FIELD_14:66;
then q gcd ((Deriv E) . q) = 1_. F by AS, B, FIELD_14:45
.= 1_. E by FIELD_4:14 ;
hence q is separable by Thsepgcd; :: thesis: verum

end;

now :: thesis: ( q is separable implies p is separable )

assume q is separable ; :: thesis: p is separable
then B: q gcd ((Deriv E) . q) = 1_. E by Thsepgcd;
(Deriv E) . q = (Deriv F) . p by AS, FIELD_14:66;
then p gcd ((Deriv F) . p) = 1_. E by AS, B, FIELD_14:45
.= 1_. F by FIELD_4:14 ;
hence p is separable by Thsepgcd; :: thesis: verum

end;

hence ( p is separable iff q is separable ) by A; :: thesis: verum