let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for a being non zero Element of F holds
( a * p is separable iff p is separable )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for a being non zero Element of F holds
( a * p is separable iff p is separable )
let c be non zero Element of F; :: thesis: ( c * p is separable iff p is separable )

A: now :: thesis: ( p is separable implies c * p is separable )

assume AS: p is separable ; :: thesis: c * p is separable

now :: thesis: for E being FieldExtension of F st c * p splits_in E holds
for a being Element of E st a is_a_root_of c * p,E holds
multiplicity ((c * p),a) = 1

let E be FieldExtension of F; :: thesis: ( c * p splits_in E implies for a being Element of E st a is_a_root_of c * p,E holds
multiplicity ((c * p),a) = 1 )
( F is Subfield of E & c <> 0. F ) by FIELD_4:7;
then H: ( c <> 0. E & @ (c,E) = c ) by EC_PF_1:def 1, FIELD_7:def 4;
then K: not @ (c,E) is zero ;
reconsider pE = p as Polynomial of E by FIELD_4:8;
I: (@ (c,E)) * pE = c * p by H, ll;
assume c * p splits_in E ; :: thesis: for a being Element of E st a is_a_root_of c * p,E holds
multiplicity ((c * p),a) = 1
then consider b being non zero Element of E, r being Ppoly of E such that
J: c * p = b * r by FIELD_4:def 5;
(@ (c,E)) * pE splits_in E by I, J, FIELD_4:def 5;
then consider b being non zero Element of E, r being Ppoly of E such that
J: pE = b * r by K, FIELD_8:9, FIELD_4:def 5;
A: p splits_in E by J, FIELD_4:def 5;
thus for a being Element of E st a is_a_root_of c * p,E holds
multiplicity ((c * p),a) = 1 :: thesis: verum

proof

let a be Element of E; :: thesis: ( a is_a_root_of c * p,E implies multiplicity ((c * p),a) = 1 )
assume a is_a_root_of c * p,E ; :: thesis: multiplicity ((c * p),a) = 1
then 0. E = Ext_eval ((c * p),a) by FIELD_4:def 2
.= (@ (c,E)) * (Ext_eval (p,a)) by FIELD_7:def 4, REALALG3:16 ;
then Ext_eval (p,a) = 0. E by H, VECTSP_2:def 1;
then multiplicity (p,a) = 1 by AS, A, ThSep0, FIELD_4:def 2;
hence multiplicity ((c * p),a) = 1 by lems1; :: thesis: verum

end;

end;

hence c * p is separable by ThSep0; :: thesis: verum

end;

now :: thesis: ( c * p is separable implies p is separable )

assume AS: c * p is separable ; :: thesis: p is separable

now :: thesis: for E being FieldExtension of F st p splits_in E holds
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1

let E be FieldExtension of F; :: thesis: ( p splits_in E implies for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 )
( F is Subfield of E & c <> 0. F ) by FIELD_4:7;
then H: ( c <> 0. E & @ (c,E) = c ) by EC_PF_1:def 1, FIELD_7:def 4;
then K: not @ (c,E) is zero ;
assume p splits_in E ; :: thesis: for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1
then consider b being non zero Element of E, r being Ppoly of E such that
J: p = b * r by FIELD_4:def 5;
c * p = (@ (c,E)) * (b * r) by H, J, ll
.= ((@ (c,E)) * b) * r by RING_4:11 ;
then A: c * p splits_in E by K, FIELD_4:def 5;
thus for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1 :: thesis: verum

proof

let a be Element of E; :: thesis: ( a is_a_root_of p,E implies multiplicity (p,a) = 1 )
assume B: a is_a_root_of p,E ; :: thesis: multiplicity (p,a) = 1
Ext_eval ((c * p),a) = (@ (c,E)) * (Ext_eval (p,a)) by REALALG3:16, FIELD_7:def 4
.= (@ (c,E)) * (0. E) by B, FIELD_4:def 2 ;
then multiplicity ((c * p),a) = 1 by AS, A, ThSep0, FIELD_4:def 2;
hence multiplicity (p,a) = 1 by lems1; :: thesis: verum

end;

end;

hence p is separable by ThSep0; :: thesis: verum

end;

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