theorem lemgcd: :: FIELD_14:45

for F being Field
for E being FieldExtension of F
for p, q being Element of the carrier of (Polynom-Ring F)
for p1, q1 being Element of the carrier of (Polynom-Ring E) st p1 = p & q1 = q holds
p1 gcd q1 = p gcd q