let F be Field; :: thesis: for p, q being Polynomial of F
for a being Element of F st q divides p & a is_a_root_of q holds
a is_a_root_of p
let p, q be Polynomial of F; :: thesis: for a being Element of F st q divides p & a is_a_root_of q holds
a is_a_root_of p
let a be Element of F; :: thesis: ( q divides p & a is_a_root_of q implies a is_a_root_of p )
assume A: ( q divides p & a is_a_root_of q ) ; :: thesis: a is_a_root_of p
then consider r being Polynomial of F such that
B: p = q *' r by RING_4:1;
eval (p,a) = (0. F) * (eval (r,a)) by A, B, POLYNOM4:24;
hence a is_a_root_of p ; :: thesis: verum