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:27
.= ((- r) + r) * (eval q,r) by POLYNOM5:48
.= (0. L) * (eval q,r) by RLVECT_1:def 11
.= 0. L by VECTSP_1:39 ;
hence r is_a_root_of p by POLYNOM5:def 6; :: thesis: verum