:: deftheorem defpmm defines poly_mult_mod RING_4:def 7 :
for F being Field
for p being Polynomial of F
for b₃ being BinOp of (Polynom-Ring F) holds
( b₃ = poly_mult_mod p iff for r, q being Polynomial of F holds b₃ . (r,q) = (r *' q) mod p );