:: deftheorem dpm defines poly_mod RING_4:def 9 :
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for b₃ being Function of (Polynom-Ring F),(Polynom-Ring p) holds
( b₃ = poly_mod p iff for q being Polynomial of F holds b₃ . q = q mod p );