let L be non degenerated comRing; :: thesis: for r being Element of L
for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds
r is_a_root_of p
let r be Element of L; :: thesis: for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds
r is_a_root_of p
let p, q be Polynomial of L; :: thesis: ( p = <%(- r),(1. L)%> *' q implies r is_a_root_of p )
assume p = <%(- r),(1. L)%> *' q ; :: thesis: r is_a_root_of p
then eval (p,r) = (eval (<%(- r),(1. L)%>,r)) * (eval (q,r)) by POLYNOM4:24
.= ((- r) + r) * (eval (q,r)) by POLYNOM5:47
.= (0. L) * (eval (q,r)) by RLVECT_1:def 10
.= 0. L ;
hence r is_a_root_of p ; :: thesis: verum