**Let
be nonzero polynomials for an Euclidean domain
.
Let
be a prime.
We denote by
the reduction
modulo
.
We know from the previous section that
**

(36) |

- .
- and are coprime in iff does not divide .

(37) |

(38) |

(39) |

(40) |

(41) |

(42) |

(43) |

(44) |

with and . If then and are both diagonal with on the diagonal. Then in that case

(45) |

If we distinguish two cases. If then (by Definition 4). Moreover each -column of is zero modulo such that too. From now on assume and let be the smallest index such that holds.

(46) |

By exchanging the -

(47) |

Let be the submatrix obtained from by deleting the last rows and the last columns. Observe that we have

(48) |

Since

(49) |

we obtain

(50) |

This shows that we have

(51) |

and the first claim of the lemma is proved. The second claim follows from Proposition 6.

(52) |

(53) |

(54) |

- divides

(55) |

we have in

(56) |

Therefore

(57) |

and the first claim is proved. Consider now the cofactors of and in

(58) |

Then we have

which shows that

(60) |

and implies that

(61) |

Since does not divide , it cannot not divide neither. Hence the leading coefficient of is and we have

(62) |

Therefore

(63) |

and the second claim is proved.

Now consider the case where . Since divides and since is monic (as a gcd over the field ) there exists a unit such that

(64) |

Since the leading coefficient of is we have in fact

(65) |

Therefore we have the following equivalence

(66) |

It remains to prove that

(67) |

Observe that cannot divide both and . If this was the case then from Relation (59) (and since does not divide ) would divide and , and thus . A contradiction. Therefore we can assume that does not divide . By applying Lemma 2 we obtain

(68) |

By applying Proposition 5 this leads to

(69) |

From Relation (59) we have

(70) |

Therefore

(71) |

This concludes the proof of the theorem.

N := NonNegativeInteger (1) NonNegativeInteger Z := Integer (2) Integer U := UnivariatePolynomial(x,Z) (3) UnivariatePolynomial(x,Integer) f: U := 12*x^3 -28*x^2 +20*x - 4 3 2 (4) 12x - 28x + 20x - 4 g: U := -12*x^2 +10*x -2 2 (5) - 12x + 10x - 2 resultant(f,g) (6) 0 h: U := gcd(f,g) (7) 6x - 2 r: Z := resultant(exquo(f,h),exquo(g,h)) (8) 2 K17 := PrimeField(17) (9) PrimeField 17 r :: K17 (10) 2 U17 := UnivariatePolynomial(x,K17) (11) UnivariatePolynomial(x,PrimeField 17) f17: U17 := f :: U17 3 2 (12) 12x + 6x + 3x + 13 g17: U17 := g :: U17 2 (13) 5x + 10x + 15 h17: U17 := h ::U17 (14) 6x + 15 c17 := gcd(f17,g17) (15) x + 11 h17 - (leadingCoefficient(h17)) * c17 (16) 0

f: U := x^4 -3*x^3 + 2*x 4 3 (4) x - 3x + 2x g: U := x^3 -1 3 (5) x - 1 resultant(f,g) (6) 0 h: U := gcd(f,g) (7) x - 1 r: Z := resultant(exquo(f,h),exquo(g,h)) (8) 9 K3 := PrimeField(3) (9) PrimeField 3 r :: K3 (10) 0 U3 := UnivariatePolynomial(x,K3) (11) UnivariatePolynomial(x,PrimeField 3) f3: U3 := f :: U3 4 (12) x + 2x g3: U3 := g :: U3 3 (13) x + 2 h3: U3 := h ::U3 (14) x + 2 c3 := gcd(f3,g3) 3 (15) x + 2 exquo(c3, h3) 2 (16) x + x + 1

*
*

2008-01-07