:: deftheorem dpg defines gcd RING_4:def 11 :
for F being Field
for p, q, b₄ being Element of the carrier of (Polynom-Ring F) holds
( ( p = 0_. F & q = 0_. F implies ( b₄ = p gcd q iff b₄ = 0_. F ) ) & ( ( not p = 0_. F or not q = 0_. F ) implies ( b₄ = p gcd q iff ( b₄ is a_gcd of p,q & b₄ is monic ) ) ) );