registration let F be Field, p be Element of the carrier of Polynom-Ring F; cluster (Polynom-Ring F)/({p}-Ideal) -> Abelian add-associative right_zeroed right_complementable commutative associative well-unital distributive; end; registration let F be Field, p be irreducible Element of the carrier of Polynom-Ring F; cluster (Polynom-Ring F)/({p}-Ideal) -> non degenerated almost_left_invertible; end; definition let F be Field, p be Polynomial of F; func poly_mult_mod p -> BinOp of Polynom-Ring F means :: RING_4:def 7 for r,q being Polynomial of F holds it.(r,q) = (r *' q) mod p; end; definition let F be Field, p be non constant Element of the carrier of Polynom-Ring F; func Polynom-Ring(p) -> strict doubleLoopStr means :: RING_4:def 8 the carrier of it = {q where q is Polynomial of F : deg q < deg p} & the addF of it = (the addF of Polynom-Ring F)||(the carrier of it) & the multF of it = (poly_mult_mod p)||(the carrier of it) & the OneF of it = 1_.(F) & the ZeroF of it = 0_.(F); end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> non degenerated; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> Abelian add-associative right_zeroed right_complementable; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> associative well-unital distributive; end; definition let F be Field, p be non constant Element of the carrier of Polynom-Ring F; func poly_mod p -> Function of Polynom-Ring F, Polynom-Ring(p) means :: RING_4:def 9 for q being Polynomial of F holds it.q = q mod p; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster poly_mod p -> additive multiplicative unity-preserving; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> (Polynom-Ring F)-homomorphic; end; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster poly_mod p -> onto; end; theorem :: RING_4:47 for F being Field, p being non constant Element of the carrier of Polynom-Ring F holds ker(poly_mod p) = {p}-Ideal; theorem :: RING_4:48 for F being Field, p being non constant Element of the carrier of Polynom-Ring F holds (Polynom-Ring F)/({p}-Ideal), Polynom-Ring(p) are_isomorphic; registration let F be Field, p be non constant Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> commutative; end; registration let F be Field, p be irreducible Element of the carrier of Polynom-Ring F; cluster Polynom-Ring(p) -> almost_left_invertible; end; begin :: Polynomial GCDs definition let L be non empty multMagma; let x,y be Element of L; let z be Element of L; attr z is x,y-gcd means :: RING_4:def 10 z divides x & z divides y & for r being Element of L st r divides x & r divides y holds r divides z; end; registration let L be gcdDomain; let x,y be Element of L; cluster x,y-gcd for Element of L; end; definition let L be gcdDomain; let x,y be Element of L; mode a_gcd of x,y is x,y-gcd Element of L; end; theorem :: RING_4:49 for L being gcdDomain for x,y being Element of L for u,v being a_gcd of x,y holds u is_associated_to v; registration let L be gcdDomain; let x,y be Element of L; cluster x,y-gcd -> y,x-gcd for Element of L; end; definition let F be Field; let p,q be Element of the carrier of Polynom-Ring F; func p gcd q -> Element of the carrier of Polynom-Ring F means :: RING_4:def 11 it = 0_.(F) if p = 0_.(F) & q = 0_.(F) otherwise it is a_gcd of p,q & it is monic; end; definition let F be Field; let p,q be Element of the carrier of Polynom-Ring F; redefine func p gcd q; commutativity; end; definition let F be Field; let p,q be Element of Polynom-Ring F; redefine func p gcd q; commutativity; end; registration let F be Field; let p,q be Element of the carrier of Polynom-Ring F; cluster p gcd q -> p,q-gcd; end; registration let F be Field; let p,q be Element of Polynom-Ring F; cluster p gcd q -> p,q-gcd; end; registration let F be Field; let p be Element of the carrier of Polynom-Ring F; let q be non zero Element of the carrier of Polynom-Ring F; cluster p gcd q -> non zero monic; end; registration let F be Field; let p be Element of Polynom-Ring F; let q be non zero Element of Polynom-Ring F; cluster p gcd q -> non zero monic; end; registration let F be Field; let p,q be zero Element of the carrier of Polynom-Ring F; cluster p gcd q -> zero; end; registration let F be Field; let p,q be zero Element of Polynom-Ring F; cluster p gcd q -> zero; end; theorem :: RING_4:50 for F being Field, p,q being Element of the carrier of Polynom-Ring F holds (p gcd q) divides p & (p gcd q) divides q & for r being Element of the carrier of Polynom-Ring F st r divides p & r divides q holds r divides (p gcd q); theorem :: RING_4:51 for F being Field, p,q being Element of Polynom-Ring F holds (p gcd q) divides p & (p gcd q) divides q & for r being Element of Polynom-Ring F st r divides p & r divides q holds r divides (p gcd q); definition let F be Field; let p,q be Polynomial of F; func p gcd q -> Polynomial of F means :: RING_4:def 12 ex a,b being Element of Polynom-Ring F st a = p & b = q & it = a gcd b; end; definition let F be Field; let p,q be Polynomial of F; redefine func p gcd q; commutativity; end; registration let F be Field; let p be Polynomial of F; let q be non zero Polynomial of F; cluster p gcd q -> non zero monic; end; registration let F be Field; let p,q be zero Polynomial of F; cluster p gcd q -> zero; end; theorem :: RING_4:52 for F being Field, p,q being Polynomial of F holds (p gcd q) divides p & (p gcd q) divides q & for r being Polynomial of F st r divides p & r divides q holds r divides (p gcd q); theorem :: RING_4:53 for F being Field for p being Polynomial of F for q being non zero Polynomial of F for s being monic Polynomial of F holds s = p gcd q iff (s divides p & s divides q & for r being Polynomial of F st r divides p & r divides q holds r divides s);