theorem diveq: :: FIELD_14:55
for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F)
for a being non zero Element of F holds MonicDivisors p = MonicDivisors (a * p)