:: Some Algebraic Properties of Polynomial Rings
:: by Christoph Schwarzweller , Artur Korni{\l}owicz and Agnieszka Rowinska-Schwarzweller
::
:: Copyright (c) 2016-2021 Association of Mizar Users

definition
let R be non empty doubleLoopStr ;
let a be Element of R;
:: original: {
redefine func {a} -> Subset of R;
coherence
{a} is Subset of R
proof end;
end;

registration
coherence
for b1 being Ring st b1 is almost_left_invertible & b1 is commutative holds
b1 is almost_right_invertible
proof end;
coherence
for b1 being Ring st b1 is almost_right_invertible & b1 is commutative holds
b1 is almost_left_invertible
proof end;
coherence
for b1 being Ring st b1 is almost_left_cancelable & b1 is commutative holds
b1 is almost_right_cancelable
proof end;
coherence
for b1 being Ring st b1 is almost_right_cancelable & b1 is commutative holds
b1 is almost_left_cancelable
proof end;
end;

definition
let L be non empty ZeroStr ;
let X be set ;
attr X is L -polynomial-membered means :polymem: :: RING_4:def 1
for p being object st p in X holds
p is Polynomial of L;
end;

:: deftheorem polymem defines -polynomial-membered RING_4:def 1 :
for L being non empty ZeroStr
for X being set holds
( X is L -polynomial-membered iff for p being object st p in X holds
p is Polynomial of L );

definition
let L be non empty ZeroStr ;
let X be 1-sorted ;
attr X is L -polynomial-membered means :polymem1: :: RING_4:def 2
the carrier of X is L -polynomial-membered ;
end;

:: deftheorem polymem1 defines -polynomial-membered RING_4:def 2 :
for L being non empty ZeroStr
for X being 1-sorted holds
( X is L -polynomial-membered iff the carrier of X is L -polynomial-membered );

registration
let L be non empty ZeroStr ;
existence
ex b1 being set st
( not b1 is empty & b1 is L -polynomial-membered )
proof end;
end;

registration
let L be non empty ZeroStr ;
existence
ex b1 being 1-sorted st
( not b1 is empty & b1 is L -polynomial-membered )
proof end;
end;

registration
let L be non empty ZeroStr ;
let X be non empty L -polynomial-membered 1-sorted ;
cluster the carrier of X -> L -polynomial-membered ;
coherence
the carrier of X is L -polynomial-membered
by polymem1;
end;

registration end;

definition
let L be non empty ZeroStr ;
let X be non empty L -polynomial-membered set ;
:: original: Element
redefine mode Element of X -> Polynomial of L;
coherence
for b1 being Element of X holds b1 is Polynomial of L
by polymem;
end;

lm: now :: thesis: for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a being Element of ()
for p being Polynomial of L st a = p holds
- a = - p
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for a being Element of ()
for p being Polynomial of L st a = p holds
- a = - p

let a be Element of (); :: thesis: for p being Polynomial of L st a = p holds
- a = - p

let p be Polynomial of L; :: thesis: ( a = p implies - a = - p )
reconsider x = - p as Element of () by POLYNOM3:def 10;
assume a = p ; :: thesis: - a = - p
then a + x = p - p by POLYNOM3:def 10
.= 0_. L by POLYNOM3:29
.= 0. () by POLYNOM3:def 10 ;
then a = - x by RLVECT_1:6;
hence - a = - p ; :: thesis: verum
end;

registration
let R be Ring;
existence
ex b1 being Element of the carrier of () st b1 is zero
proof end;
existence
ex b1 being Element of () st b1 is zero
proof end;
cluster V1() V4( NAT ) V5( the carrier of R) Function-like non empty total quasi_total finite-Support zero for Element of bool [:NAT, the carrier of R:];
existence
ex b1 being Polynomial of R st b1 is zero
proof end;
end;

registration
let R be non degenerated Ring;
existence
not for b1 being Element of the carrier of () holds b1 is zero
proof end;
existence
not for b1 being Element of () holds b1 is zero
proof end;
end;

T8a: for L being non trivial right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being Element of the carrier of () holds
( deg p is Element of NAT iff p <> 0. () )

proof end;

T8b: for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )

proof end;

definition
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
let p, q be Polynomial of L;
pred p divides q means :: RING_4:def 3
ex a, b being Element of () st
( a = p & b = q & a divides b );
end;

:: deftheorem defines divides RING_4:def 3 :
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p, q being Polynomial of L holds
( p divides q iff ex a, b being Element of () st
( a = p & b = q & a divides b ) );

theorem T2: :: RING_4:1
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p, q being Polynomial of L holds
( p divides q iff ex r being Polynomial of L st p *' r = q )
proof end;

theorem div1: :: RING_4:2
for F being Field
for p, q being Polynomial of F st deg p < deg q holds
p mod q = p
proof end;

div0: for F being Field
for p, q being Polynomial of F st q divides p holds
(p div q) *' q = p

proof end;

theorem div2: :: RING_4:3
for F being Field
for p, q being Polynomial of F holds
( p mod q = 0_. F iff q divides p )
proof end;

theorem div5: :: RING_4:4
for F being Field
for p, q being Polynomial of F holds p = ((p div q) *' q) + (p mod q)
proof end;

theorem div4: :: RING_4:5
for F being Field
for p, r being Polynomial of F
for q being non zero Polynomial of F holds
( (p + r) div q = (p div q) + (r div q) & (p + r) mod q = (p mod q) + (r mod q) )
proof end;

theorem div3a: :: RING_4:6
for F being Field
for p, r being Polynomial of F
for q being non zero Polynomial of F holds (p *' r) mod q = ((p mod q) *' (r mod q)) mod q
proof end;

theorem div3: :: RING_4:7
for F being Field
for r, q, u being Polynomial of F
for p being non zero Polynomial of F holds (((r *' q) mod p) *' u) mod p = ((r *' q) *' u) mod p
proof end;

theorem :: RING_4:8
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being sequence of L holds (0. L) * p = 0_. L
proof end;

theorem poly2a: :: RING_4:9
for L being non empty left_unital doubleLoopStr
for p being sequence of L holds (1. L) * p = p
proof end;

theorem poly2: :: RING_4:10
for L being non empty right_complementable add-associative right_zeroed right_unital distributive associative commutative doubleLoopStr
for p, q being sequence of L
for a being Element of L holds a * (p *' q) = p *' (a * q)
proof end;

theorem poly3: :: RING_4:11
for L being non empty associative multMagma
for p being sequence of L
for a, b being Element of L holds (a * b) * p = a * (b * p)
proof end;

theorem poly1: :: RING_4:12
for L being non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr
for p being sequence of L holds (1_. L) *' p = p
proof end;

registration end;

definition
let R be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
let x be Element of the carrier of ();
attr x is constant means :defconst: :: RING_4:def 4
deg x <= 0 ;
end;

:: deftheorem defconst defines constant RING_4:def 4 :
for R being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for x being Element of the carrier of () holds
( x is constant iff deg x <= 0 );

registration
let R be non degenerated Ring;
existence
ex b1 being Element of () st
( not b1 is zero & b1 is constant )
proof end;
existence
ex b1 being Element of the carrier of () st
( not b1 is zero & b1 is constant )
proof end;
end;

registration
let R be domRing;
existence
not for b1 being Element of () holds b1 is constant
proof end;
existence
not for b1 being Element of the carrier of () holds b1 is constant
proof end;
end;

definition
let L be non empty ZeroStr ;
let a be Element of L;
func a | L -> sequence of L equals :: RING_4:def 5
(0_. L) +* (0,a);
coherence
(0_. L) +* (0,a) is sequence of L
;
end;

:: deftheorem defines | RING_4:def 5 :
for L being non empty ZeroStr
for a being Element of L holds a | L = (0_. L) +* (0,a);

registration
let L be non empty ZeroStr ;
let a be Element of L;
coherence
a | L is finite-Support
proof end;
end;

Th28: for L being non empty ZeroStr
for a being Element of L holds
( (a | L) . 0 = a & ( for n being Nat st n <> 0 holds
(a | L) . n = 0. L ) )

proof end;

T6: for L being non empty ZeroStr holds (0. L) | L = 0_. L
proof end;

registration
let L be non empty ZeroStr ;
let a be Element of L;
cluster a | L -> constant ;
coherence
a | L is constant
proof end;
end;

registration
let L be non trivial ZeroStr ;
let a be non zero Element of L;
cluster a | L -> non zero ;
coherence
not a | L is zero
proof end;
end;

registration
let L be non trivial ZeroStr ;
cluster V1() V4( NAT ) V5( the carrier of L) Function-like non empty total quasi_total finite-Support non zero constant for Element of bool [:NAT, the carrier of L:];
existence
ex b1 being Polynomial of L st
( not b1 is zero & b1 is constant )
proof end;
end;

theorem :: RING_4:13
for L being non empty ZeroStr holds (0. L) | L = 0_. L by T6;

theorem :: RING_4:14
for L being non empty multLoopStr_0 holds (1. L) | L = 1_. L ;

registration
let L be non empty ZeroStr ;
cluster (0. L) | L -> zero ;
coherence
(0. L) | L is zero
by T6;
end;

registration
let L be non degenerated multLoopStr_0 ;
cluster (1. L) | L -> non zero ;
coherence
not (1. L) | L is zero
;
end;

theorem LX: :: RING_4:15
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being Element of the carrier of () holds
( ( not p is zero & p is constant ) iff deg p = 0 )
proof end;

theorem LX1: :: RING_4:16
for L being non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr
for a being Element of L holds a | L = a * (1_. L)
proof end;

theorem T4a: :: RING_4:17
for R being Ring
for a, b being Element of R holds (a | R) + (b | R) = (a + b) | R
proof end;

theorem T4: :: RING_4:18
for R being Ring
for a, b being Element of R holds (a | R) *' (b | R) = (a * b) | R
proof end;

theorem T9: :: RING_4:19
for R being Ring
for a, b being Element of R holds
( a | R = b | R iff a = b )
proof end;

theorem T11: :: RING_4:20
for R being Ring
for p being Element of the carrier of () holds
( p is constant iff ex a being Element of R st p = a | R )
proof end;

theorem T11a: :: RING_4:21
for R being Ring
for a being Element of R holds
( deg (a | R) = 0 iff a <> 0. R )
proof end;

notation
let L be non empty doubleLoopStr ;
let p be Polynomial of L;
synonym monic p for normalized ;
end;

registration
let L be non degenerated doubleLoopStr ;
cluster 1_. L -> monic ;
coherence
1_. L is monic
proof end;
cluster 0_. L -> non monic ;
coherence
not 0_. L is monic
proof end;
end;

registration
let L be non degenerated doubleLoopStr ;
cluster V1() V4( NAT ) V5( the carrier of L) Function-like non empty total quasi_total finite-Support monic for Element of bool [:NAT, the carrier of L:];
existence
ex b1 being Polynomial of L st b1 is monic
proof end;
cluster V1() V4( NAT ) V5( the carrier of L) Function-like non empty total quasi_total finite-Support non monic for Element of bool [:NAT, the carrier of L:];
existence
not for b1 being Polynomial of L holds b1 is monic
proof end;
end;

registration
let L be non degenerated right_complementable add-associative right_zeroed distributive doubleLoopStr ;
existence
ex b1 being Element of the carrier of () st b1 is monic
proof end;
existence
not for b1 being Element of the carrier of () holds b1 is monic
proof end;
end;

registration
let L be non degenerated well-unital doubleLoopStr ;
let x be Element of L;
cluster rpoly (1,x) -> monic ;
coherence
rpoly (1,x) is monic
proof end;
end;

definition
let L be Field;
let p be Element of the carrier of ();
:: original: NormPolynomial
redefine func NormPolynomial p -> Element of the carrier of ();
coherence
NormPolynomial p is Element of the carrier of ()
by POLYNOM3:def 10;
end;

registration
let F be Field;
let p be non zero Polynomial of F;
coherence ;
end;

registration
let L be Field;
let p be non zero Element of the carrier of ();
coherence ;
end;

theorem npl0: :: RING_4:22
for F being Field holds NormPolynomial (0_. F) = 0_. F
proof end;

theorem npl: :: RING_4:23
for F being Field
for p being non zero Element of the carrier of () holds NormPolynomial p = ((LC p) ") * p
proof end;

theorem :: RING_4:24
for F being Field
for p being non zero Element of the carrier of () holds
( p is monic iff NormPolynomial p = p )
proof end;

theorem np1: :: RING_4:25
for F being Field
for p, q being Element of the carrier of () holds
( q divides p iff NormPolynomial q divides p )
proof end;

theorem np2: :: RING_4:26
for F being Field
for p, q being Element of the carrier of () holds
( q divides p iff q divides NormPolynomial p )
proof end;

theorem np3: :: RING_4:27
for F being Field
for p being Element of the carrier of () holds NormPolynomial p is_associated_to p
proof end;

theorem thirr2: :: RING_4:28
for F being Field
for p being Element of the carrier of () holds
( NormPolynomial p is irreducible iff p is irreducible )
proof end;

theorem np00: :: RING_4:29
for R being domRing
for p, q being Element of the carrier of () st p is_associated_to q holds
deg p = deg q
proof end;

theorem np0: :: RING_4:30
for R being domRing
for p, q being monic Element of the carrier of () holds
( p is_associated_to q iff p = q )
proof end;

definition
let R be Ring;
func canHom R -> Function of R,() means :defcanhom: :: RING_4:def 6
for x being Element of R holds it . x = x | R;
existence
ex b1 being Function of R,() st
for x being Element of R holds b1 . x = x | R
proof end;
uniqueness
for b1, b2 being Function of R,() st ( for x being Element of R holds b1 . x = x | R ) & ( for x being Element of R holds b2 . x = x | R ) holds
b1 = b2
proof end;
end;

:: deftheorem defcanhom defines canHom RING_4:def 6 :
for R being Ring
for b2 being Function of R,() holds
( b2 = canHom R iff for x being Element of R holds b2 . x = x | R );

registration
let R be Ring;
coherence
proof end;
end;

registration
let R be Ring;
coherence
proof end;
end;

registration
let R be Ring;
coherence
proof end;
end;

theorem :: RING_4:31
for R being Ring holds Char () = Char R by RING_3:88;

registration
let R be non degenerated Ring;
coherence
not Polynom-Ring R is finite
proof end;
end;

registration
coherence
for b1 being 0 -characteristic Ring holds b1 is infinite
proof end;
end;

theorem :: RING_4:32
for R being Ring st Char R = 0 holds
R is infinite
proof end;

registration
let n be non trivial Nat;
coherence
not Polynom-Ring (Z/ n) is finite
;
end;

theorem :: RING_4:33
for n being non trivial Nat holds Char (Polynom-Ring (Z/ n)) <> 0 ;

registration
let n be non trivial Nat;
existence
ex b1 being Ring st
( b1 is n -characteristic & b1 is infinite )
proof end;
end;

lemr: for R being domRing holds not Polynom-Ring R is almost_left_invertible
proof end;

registration
existence
not for b1 being domRing holds b1 is almost_left_invertible
proof end;
end;

lemf: for R being domRing holds
( R is Field iff for a being NonUnit of R holds a = 0. R )

proof end;

registration
let R be non almost_left_invertible domRing;
existence
not for b1 being NonUnit of R holds b1 is zero
proof end;
end;

registration
coherence
proof end;
end;

registration
let R be domRing;
coherence by lemr;
end;

theorem :: RING_4:34
for R being domRing holds
( R is Field iff for a being NonUnit of R holds a = 0. R ) by lemf;

theorem Th90: :: RING_4:35
for R being domRing
for a being Element of R holds
( a | R is Unit of () iff a is Unit of R )
proof end;

theorem T88: :: RING_4:36
for F being domRing
for p being Element of the carrier of () st p is Unit of () holds
deg p = 0
proof end;

theorem T8: :: RING_4:37
for F being Field
for p being Element of the carrier of () holds
( p is Unit of () iff deg p = 0 )
proof end;

theorem :: RING_4:38
for R being domRing
for p being Element of the carrier of () st p is Unit of () holds
( not p is zero & p is constant )
proof end;

theorem :: RING_4:39
for F being Field
for p being Element of the carrier of () holds
( p is Unit of () iff ( not p is zero & p is constant ) )
proof end;

registration
let R be domRing;
cluster non constant -> non zero non unital for Element of the carrier of ();
coherence
for b1 being Element of () st not b1 is constant holds
( not b1 is zero & not b1 is unital )
proof end;
end;

registration
let F be domRing;
cluster non constant -> non zero non unital for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st not b1 is constant holds
( not b1 is zero & not b1 is unital )
proof end;
end;

registration
let F be Field;
cluster non zero constant -> unital for Element of the carrier of ();
coherence
for b1 being Element of () st not b1 is zero & b1 is constant holds
b1 is unital
proof end;
cluster unital -> non zero constant for Element of the carrier of ();
coherence
for b1 being Element of () st b1 is unital holds
( not b1 is zero & b1 is constant )
;
end;

registration
let F be Field;
cluster non zero constant -> unital for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st not b1 is zero & b1 is constant holds
b1 is unital
proof end;
cluster unital -> non zero constant for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st b1 is unital holds
( not b1 is zero & b1 is constant )
proof end;
end;

theorem T88a: :: RING_4:40
for R being domRing
for p being Element of the carrier of () st ex q being Element of the carrier of () st
( q divides p & 1 <= deg q & deg q < deg p ) holds
p is reducible
proof end;

theorem T88b: :: RING_4:41
for F being Field
for p being Element of the carrier of () holds
( ( p = 0_. F or p is Unit of () or ex q being Element of the carrier of () st
( q divides p & 1 <= deg q & deg q < deg p ) ) iff p is reducible )
proof end;

theorem thirr0: :: RING_4:42
for R being domRing
for p being monic Element of the carrier of () st deg p = 1 holds
p is irreducible
proof end;

theorem :: RING_4:43
ex p being non monic Element of the carrier of st
( deg p = 1 & p is reducible )
proof end;

theorem thirr: :: RING_4:44
for F being Field
for p being Element of the carrier of () st deg p = 1 holds
p is irreducible
proof end;

theorem thirr1: :: RING_4:45
for F being algebraic-closed Field
for p being Element of the carrier of () holds
( p is irreducible iff deg p = 1 )
proof end;

theorem :: RING_4:46
for F being Field holds
( F is algebraic-closed iff for p being monic Element of the carrier of () holds
( p is irreducible iff deg p = 1 ) )
proof end;

registration
let R be domRing;
existence
ex b1 being Element of () st b1 is irreducible
proof end;
end;

registration
let R be domRing;
existence
ex b1 being Element of the carrier of () st b1 is irreducible
proof end;
end;

registration
let R be Ring;
existence
ex b1 being Element of () st b1 is reducible
proof end;
end;

registration
let R be Ring;
existence
ex b1 being Element of the carrier of () st b1 is reducible
proof end;
end;

registration
let R be domRing;
cluster IRR () -> non empty ;
coherence
not IRR () is empty
proof end;
end;

registration
let F be Field;
cluster constant -> reducible for Element of the carrier of ();
coherence
for b1 being Element of () st b1 is constant holds
b1 is reducible
;
end;

registration
let F be Field;
cluster constant -> reducible for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st b1 is constant holds
b1 is reducible
;
end;

registration
let F be Field;
cluster irreducible -> non constant for Element of the carrier of ();
coherence
for b1 being Element of () st b1 is irreducible holds
not b1 is constant
;
end;

registration
let F be Field;
cluster irreducible -> non constant for Element of the carrier of ();
coherence
for b1 being Element of the carrier of () st b1 is irreducible holds
not b1 is constant
;
end;

registration
let F be Field;
let p be Element of the carrier of ();
coherence
( () / () is Abelian & () / () is add-associative & () / () is right_zeroed & () / () is right_complementable & () / () is commutative & () / () is associative & () / () is well-unital & () / () is distributive )
;
end;

registration
let F be Field;
let p be irreducible Element of the carrier of ();
coherence
( not () / () is degenerated & () / () is almost_left_invertible )
by ;
end;

definition
let F be Field;
let p be Polynomial of F;
func poly_mult_mod p -> BinOp of () means :defpmm: :: RING_4:def 7
for r, q being Polynomial of F holds it . (r,q) = (r *' q) mod p;
existence
ex b1 being BinOp of () st
for r, q being Polynomial of F holds b1 . (r,q) = (r *' q) mod p
proof end;
uniqueness
for b1, b2 being BinOp of () st ( for r, q being Polynomial of F holds b1 . (r,q) = (r *' q) mod p ) & ( for r, q being Polynomial of F holds b2 . (r,q) = (r *' q) mod p ) holds
b1 = b2
proof end;
end;

:: deftheorem defpmm defines poly_mult_mod RING_4:def 7 :
for F being Field
for p being Polynomial of F
for b3 being BinOp of () holds
( b3 = poly_mult_mod p iff for r, q being Polynomial of F holds b3 . (r,q) = (r *' q) mod p );

pr1: for F being Field
for p being Element of the carrier of () holds { q where q is Polynomial of F : deg q < deg p } is Preserv of the addF of ()

proof end;

pr2: for F being Field
for p being non constant Element of the carrier of () holds { q where q is Polynomial of F : deg q < deg p } is Preserv of poly_mult_mod p

proof end;

pr3: for F being Field
for p being non constant Element of the carrier of () holds 1_. F in { q where q is Polynomial of F : deg q < deg p }

proof end;

pr4: for F being Field
for p being non constant Element of the carrier of () holds 0_. F in { q where q is Polynomial of F : deg q < deg p }

proof end;

definition
let F be Field;
let p be non constant Element of the carrier of ();
func Polynom-Ring p -> strict doubleLoopStr means :defprfp: :: 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 () || the carrier of it & the multF of it = () || the carrier of it & the OneF of it = 1_. F & the ZeroF of it = 0_. F );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = { q where q is Polynomial of F : deg q < deg p } & the addF of b1 = the addF of () || the carrier of b1 & the multF of b1 = () || the carrier of b1 & the OneF of b1 = 1_. F & the ZeroF of b1 = 0_. F )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = { q where q is Polynomial of F : deg q < deg p } & the addF of b1 = the addF of () || the carrier of b1 & the multF of b1 = () || the carrier of b1 & the OneF of b1 = 1_. F & the ZeroF of b1 = 0_. F & the carrier of b2 = { q where q is Polynomial of F : deg q < deg p } & the addF of b2 = the addF of () || the carrier of b2 & the multF of b2 = () || the carrier of b2 & the OneF of b2 = 1_. F & the ZeroF of b2 = 0_. F holds
b1 = b2
;
end;

:: deftheorem defprfp defines Polynom-Ring RING_4:def 8 :
for F being Field
for p being non constant Element of the carrier of ()
for b3 being strict doubleLoopStr holds
( b3 = Polynom-Ring p iff ( the carrier of b3 = { q where q is Polynomial of F : deg q < deg p } & the addF of b3 = the addF of () || the carrier of b3 & the multF of b3 = () || the carrier of b3 & the OneF of b3 = 1_. F & the ZeroF of b3 = 0_. F ) );

registration
let F be Field;
let p be non constant Element of the carrier of ();
coherence
not Polynom-Ring p is degenerated
proof end;
end;

registration
let F be Field;
let p be non constant Element of the carrier of ();
coherence
proof end;
end;

registration
let F be Field;
let p be non constant Element of the carrier of ();
coherence
proof end;
end;

definition
let F be Field;
let p be non constant Element of the carrier of ();
func poly_mod p -> Function of (),() means :dpm: :: RING_4:def 9
for q being Polynomial of F holds it . q = q mod p;
existence
ex b1 being Function of (),() st
for q being Polynomial of F holds b1 . q = q mod p
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for q being Polynomial of F holds b1 . q = q mod p ) & ( for q being Polynomial of F holds b2 . q = q mod p ) holds
b1 = b2
proof end;
end;

:: deftheorem dpm defines poly_mod RING_4:def 9 :
for F being Field
for p being non constant Element of the carrier of ()
for b3 being Function of (),() holds
( b3 = poly_mod p iff for q being Polynomial of F holds b3 . q = q mod p );

registration
let F be Field;
let p be non constant Element of the carrier of ();
coherence
proof end;
end;

registration
let F be Field;
let p be non constant Element of the carrier of ();
coherence
proof end;
end;

registration
let F be Field;
let p be non constant Element of the carrier of ();
coherence
poly_mod p is onto
proof end;
end;

lemminuspoly: for R being Ring
for a being Element of ()
for b being Polynomial of R st a = b holds
- a = - b

proof end;

theorem kerp: :: RING_4:47
for F being Field
for p being non constant Element of the carrier of () holds ker () = {p} -Ideal
proof end;

theorem ISO: :: RING_4:48
for F being Field
for p being non constant Element of the carrier of () holds () / (), Polynom-Ring p are_isomorphic
proof end;

registration
let F be Field;
let p be non constant Element of the carrier of ();
coherence
proof end;
end;

registration
let F be Field;
let p be irreducible Element of the carrier of ();
coherence
proof end;
end;

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 :defGCD: :: 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;

:: deftheorem defGCD defines -gcd RING_4:def 10 :
for L being non empty multMagma
for x, y, z being Element of L holds
( z is x,y -gcd iff ( z divides x & z divides y & ( for r being Element of L st r divides x & r divides y holds
r divides z ) ) );

registration
let L be gcdDomain;
let x, y be Element of L;
existence
ex b1 being Element of L st b1 is x,y -gcd
proof end;
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 gcd1: :: 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
proof end;

registration
let L be gcdDomain;
let x, y be Element of L;
cluster x,y -gcd -> y,x -gcd for Element of the carrier of L;
coherence
for b1 being Element of L st b1 is x,y -gcd holds
b1 is y,x -gcd
;
end;

definition
let F be Field;
let p, q be Element of the carrier of ();
func p gcd q -> Element of the carrier of () means :dpg: :: 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 );
existence
( ( p = 0_. F & q = 0_. F implies ex b1 being Element of the carrier of () st b1 = 0_. F ) & ( ( not p = 0_. F or not q = 0_. F ) implies ex b1 being Element of the carrier of () st
( b1 is a_gcd of p,q & b1 is monic ) ) )
proof end;
uniqueness
for b1, b2 being Element of the carrier of () holds
( ( p = 0_. F & q = 0_. F & b1 = 0_. F & b2 = 0_. F implies b1 = b2 ) & ( ( not p = 0_. F or not q = 0_. F ) & b1 is a_gcd of p,q & b1 is monic & b2 is a_gcd of p,q & b2 is monic implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of the carrier of () holds verum
;
end;

:: deftheorem dpg defines gcd RING_4:def 11 :
for F being Field
for p, q, b4 being Element of the carrier of () holds
( ( p = 0_. F & q = 0_. F implies ( b4 = p gcd q iff b4 = 0_. F ) ) & ( ( not p = 0_. F or not q = 0_. F ) implies ( b4 = p gcd q iff ( b4 is a_gcd of p,q & b4 is monic ) ) ) );

definition
let F be Field;
let p, q be Element of the carrier of ();
:: original: gcd
redefine func p gcd q -> Element of the carrier of ();
commutativity
for p, q being Element of the carrier of () holds p gcd q = q gcd p
proof end;
end;

definition
let F be Field;
let p, q be Element of ();
:: original: gcd
redefine func p gcd q -> Element of the carrier of ();
commutativity
for p, q being Element of () holds p gcd q = q gcd p
proof end;
end;

registration
let F be Field;
let p, q be Element of the carrier of ();
cluster p gcd q -> p,q -gcd ;
coherence
p gcd q is p,q -gcd
proof end;
end;

registration
let F be Field;
let p, q be Element of ();
cluster p gcd q -> p,q -gcd ;
coherence
p gcd q is p,q -gcd
;
end;

registration
let F be Field;
let p be Element of the carrier of ();
let q be non zero Element of the carrier of ();
cluster p gcd q -> non zero monic ;
coherence
( not p gcd q is zero & p gcd q is monic )
proof end;
end;

registration
let F be Field;
let p be Element of ();
let q be non zero Element of ();
cluster p gcd q -> non zero monic ;
coherence
( not p gcd q is zero & p gcd q is monic )
proof end;
end;

registration
let F be Field;
let p, q be zero Element of the carrier of ();
cluster p gcd q -> zero ;
coherence
p gcd q is zero
proof end;
end;

registration
let F be Field;
let p, q be zero Element of ();
cluster p gcd q -> zero ;
coherence
p gcd q is zero
proof end;
end;

theorem :: RING_4:50
for F being Field
for p, q being Element of the carrier of () holds
( p gcd q divides p & p gcd q divides q & ( for r being Element of the carrier of () st r divides p & r divides q holds
r divides p gcd q ) )
proof end;

theorem :: RING_4:51
for F being Field
for p, q being Element of () holds
( p gcd q divides p & p gcd q divides q & ( for r being Element of () st r divides p & r divides q holds
r divides p gcd q ) ) by defGCD;

definition
let F be Field;
let p, q be Polynomial of F;
func p gcd q -> Polynomial of F means :dd: :: RING_4:def 12
ex a, b being Element of () st
( a = p & b = q & it = a gcd b );
existence
ex b1 being Polynomial of F ex a, b being Element of () st
( a = p & b = q & b1 = a gcd b )
proof end;
uniqueness
for b1, b2 being Polynomial of F st ex a, b being Element of () st
( a = p & b = q & b1 = a gcd b ) & ex a, b being Element of () st
( a = p & b = q & b2 = a gcd b ) holds
b1 = b2
;
end;

:: deftheorem dd defines gcd RING_4:def 12 :
for F being Field
for p, q, b4 being Polynomial of F holds
( b4 = p gcd q iff ex a, b being Element of () st
( a = p & b = q & b4 = a gcd b ) );

definition
let F be Field;
let p, q be Polynomial of F;
:: original: gcd
redefine func p gcd q -> Polynomial of F;
commutativity
for p, q being Polynomial of F holds p gcd q = q gcd p
proof end;
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 ;
coherence
( not p gcd q is zero & p gcd q is monic )
proof end;
end;

registration
let F be Field;
let p, q be zero Polynomial of F;
cluster p gcd q -> zero ;
coherence
p gcd q is zero
proof end;
end;

theorem G1: :: RING_4:52
for F being Field
for 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 ) )
proof end;

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 ) ) )
proof end;