theorem lemgcdn: :: FIELD_14:47

for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for q being non zero Element of the carrier of (Polynom-Ring F) st q divides p holds
p gcd q = NormPolynomial q