:: deftheorem dd defines gcd RING_4:def 12 :
for F being Field
for p, q, b₄ being Polynomial of F holds
( b₄ = p gcd q iff ex a, b being Element of (Polynom-Ring F) st
( a = p & b = q & b₄ = a gcd b ) );