let R be domRing; for p, q being monic Element of the carrier of (Polynom-Ring R) holds
( p is_associated_to q iff p = q )
let p, q be monic Element of the carrier of (Polynom-Ring R); ( p is_associated_to q iff p = q )
K1:
( LC p = 1. R & LC q = 1. R )
by RATFUNC1:def 7;
now ( p is_associated_to q implies p = q )assume AS:
p is_associated_to q
;
p = qthen consider c being
Element of
(Polynom-Ring R) such that K2:
q = p * c
by GCD_1:def 1;
reconsider r =
c as
Element of the
carrier of
(Polynom-Ring R) ;
K3:
q = p *' r
by K2, POLYNOM3:def 10;
r <> 0_. R
by K3, POLYNOM3:34;
then deg q =
(deg p) + (deg r)
by K3, HURWITZ:23
.=
(deg q) + (deg r)
by AS, np00
;
then
r is
constant
;
then consider a being
Element of
R such that K5:
r = a | R
by T11;
X:
deg p = deg q
by AS, np00;
r = a * (1_. R)
by K5, LX1;
then q =
a * (p *' (1_. R))
by K3, poly2
.=
a * p
by poly1
;
then q . ((len q) -' 1) =
a * (1. R)
by X, K1, POLYNOM5:def 4
.=
a
;
then
r = 1_. R
by K5, K1;
hence
p = q
by K3, poly1;
verum end;
hence
( p is_associated_to q iff p = q )
; verum