:: deftheorem defprfp defines Polynom-Ring RING_4:def 8 :
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for b₃ being strict doubleLoopStr holds
( b₃ = Polynom-Ring p iff ( the carrier of b₃ = { q where q is Polynomial of F : deg q < deg p } & the addF of b₃ = the addF of (Polynom-Ring F) || the carrier of b₃ & the multF of b₃ = (poly_mult_mod p) || the carrier of b₃ & the OneF of b₃ = 1_. F & the ZeroF of b₃ = 0_. F ) );