:: deftheorem defines Divisors FIELD_14:def 4 :
for R being domRing
for p being Polynomial of R holds Divisors p = { q where q is Element of the carrier of (Polynom-Ring R) : q divides p } ;