let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( p is separable iff for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 )
set E = the SplittingField of p;

A: now :: thesis: ( p is separable implies for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 )

assume B: p is separable ; :: thesis: for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1
thus for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 :: thesis: verum

proof

let a be Element of the SplittingField of p; :: thesis: multiplicity (p,a) <= 1

per cases ( a is_a_root_of p, the SplittingField of p or not a is_a_root_of p, the SplittingField of p ) ;

suppose a is_a_root_of p, the SplittingField of p ; :: thesis: multiplicity (p,a) <= 1

hence multiplicity (p,a) <= 1 by B; :: thesis: verum

end;

suppose not a is_a_root_of p, the SplittingField of p ; :: thesis: multiplicity (p,a) <= 1

hence multiplicity (p,a) <= 1 by mulzero; :: thesis: verum

end;

end;

end;

end;

now :: thesis: ( ( for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 ) implies p is separable )

assume B: for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 ; :: thesis: p is separable

now :: thesis: for a being Element of the SplittingField of p st a is_a_root_of p, the SplittingField of p holds
multiplicity (p,a) = 1

let a be Element of the SplittingField of p; :: thesis: ( a is_a_root_of p, the SplittingField of p implies multiplicity (p,a) = 1 )
assume a is_a_root_of p, the SplittingField of p ; :: thesis: multiplicity (p,a) = 1
then C: multiplicity (p,a) >= 1 by mulzero;
multiplicity (p,a) <= 1 by B;
hence multiplicity (p,a) = 1 by C, XXREAL_0:1; :: thesis: verum

end;

hence p is separable ; :: thesis: verum

end;

hence ( p is separable iff for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 ) by A; :: thesis: verum