theorem R441: :: FIELD_15:18

for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F) holds
( ( p is Unit of (Polynom-Ring F) or ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) ) iff p is reducible )