theorem :: RING_4:53

for F being Field
for p being Polynomial of F
for q being non zero Polynomial of F
for s being monic Polynomial of F holds
( s = p gcd q iff ( s divides p & s divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides s ) ) )