:: by Christoph Schwarzweller , Artur Korni{\l}owicz and Agnieszka Rowinska-Schwarzweller

::

:: Received June 30, 2016

:: Copyright (c) 2016-2018 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

end;
let a be Element of R;

:: original: {

redefine func {a} -> Subset of R;

coherence

{a} is Subset of R

proof end;

registration

for b_{1} being Ring st b_{1} is almost_left_invertible & b_{1} is commutative holds

b_{1} is almost_right_invertible

for b_{1} being Ring st b_{1} is almost_right_invertible & b_{1} is commutative holds

b_{1} is almost_left_invertible

for b_{1} being Ring st b_{1} is almost_left_cancelable & b_{1} is commutative holds

b_{1} is almost_right_cancelable

for b_{1} being Ring st b_{1} is almost_right_cancelable & b_{1} is commutative holds

b_{1} is almost_left_cancelable
end;

cluster non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative -> almost_right_invertible for Ring;

coherence for b

b

proof end;

cluster non empty right_complementable almost_right_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative -> almost_left_invertible for Ring;

coherence for b

b

proof end;

cluster non empty right_complementable almost_left_cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative -> almost_right_cancelable for Ring;

coherence for b

b

proof end;

cluster non empty right_complementable almost_right_cancelable Abelian add-associative right_zeroed well-unital distributive associative commutative -> almost_left_cancelable for Ring;

coherence for b

b

proof end;

definition

let L be non empty ZeroStr ;

let X be set ;

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

for p being object st p in X holds

p is Polynomial of L;

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

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 ;

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

the carrier of X is L -polynomial-membered ;

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

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 b_{1} being set st

( not b_{1} is empty & b_{1} is L -polynomial-membered )

end;
existence

ex b

( not b

proof end;

registration

let L be non empty ZeroStr ;

existence

ex b_{1} being 1-sorted st

( not b_{1} is empty & b_{1} is L -polynomial-membered )

end;
existence

ex b

( not b

proof end;

registration

let L be non empty ZeroStr ;

let X be non empty L -polynomial-membered 1-sorted ;

coherence

the carrier of X is L -polynomial-membered by polymem1;

end;
let X be non empty L -polynomial-membered 1-sorted ;

coherence

the carrier of X is L -polynomial-membered by polymem1;

registration

let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;

coherence

Polynom-Ring L is L -polynomial-membered

end;
coherence

Polynom-Ring L is L -polynomial-membered

proof 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 b_{1} being Element of X holds b_{1} is Polynomial of L
by polymem;

end;
let X be non empty L -polynomial-membered set ;

:: original: Element

redefine mode Element of X -> Polynomial of L;

coherence

for b

lm: now :: thesis: for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr

for a being Element of (Polynom-Ring L)

for p being Polynomial of L st a = p holds

- a = - p

for a being Element of (Polynom-Ring L)

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 (Polynom-Ring L)

for p being Polynomial of L st a = p holds

- a = - p

let a be Element of (Polynom-Ring L); :: 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 (Polynom-Ring L) 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. (Polynom-Ring L) by POLYNOM3:def 10 ;

then a = - x by RLVECT_1:6;

hence - a = - p ; :: thesis: verum

end;
for p being Polynomial of L st a = p holds

- a = - p

let a be Element of (Polynom-Ring L); :: 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 (Polynom-Ring L) 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. (Polynom-Ring L) by POLYNOM3:def 10 ;

then a = - x by RLVECT_1:6;

hence - a = - p ; :: thesis: verum

registration

let R be Ring;

ex b_{1} being Element of the carrier of (Polynom-Ring R) st b_{1} is zero

ex b_{1} being Element of (Polynom-Ring R) st b_{1} is zero

ex b_{1} being Polynomial of R st b_{1} is zero

end;
cluster V1() V4( NAT ) V5( the carrier of R) Function-like non empty total quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support zero for of ;

existence ex b

proof end;

cluster zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable for Element of (Polynom-Ring R);

existence ex b

proof end;

cluster V1() V4( NAT ) V5( the carrier of R) Function-like non empty total quasi_total finite-Support zero for Polynomial of ;

existence ex b

proof end;

registration

let R be non degenerated Ring;

not for b_{1} being Element of the carrier of (Polynom-Ring R) holds b_{1} is zero

not for b_{1} being Element of (Polynom-Ring R) holds b_{1} is zero

end;
cluster V1() V4( NAT ) V5( the carrier of R) Function-like non empty total quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non zero for of ;

existence not for b

proof end;

cluster non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable for Element of (Polynom-Ring R);

existence not for b

proof end;

T8a: for L being non trivial right_complementable add-associative right_zeroed distributive doubleLoopStr

for p being Element of the carrier of (Polynom-Ring L) holds

( deg p is Element of NAT iff p <> 0. (Polynom-Ring L) )

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;

end;
let p, q be Polynomial of L;

pred p divides q means :: RING_4:def 3

ex a, b being Element of (Polynom-Ring L) st

( a = p & b = q & a divides b );

ex a, b being Element of (Polynom-Ring L) st

( a = p & b = q & a divides b );

:: 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 (Polynom-Ring L) st

( a = p & b = q & a divides b ) );

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 (Polynom-Ring L) 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 )

for p, q being Polynomial of L holds

( p divides q iff ex r being Polynomial of L st p *' r = q )

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 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) )

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

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

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

for p being sequence of L holds (0. L) * p = 0_. L

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)

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)

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

for p being sequence of L holds (1_. L) *' p = p

proof end;

registration

let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;

coherence

Polynom-Ring L is well-unital

end;
coherence

Polynom-Ring L is well-unital

proof end;

definition

let R be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;

let x be Element of the carrier of (Polynom-Ring R);

end;
let x be Element of the carrier of (Polynom-Ring R);

:: 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 (Polynom-Ring R) holds

( x is constant iff deg x <= 0 );

for R being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr

for x being Element of the carrier of (Polynom-Ring R) holds

( x is constant iff deg x <= 0 );

registration

let R be non degenerated Ring;

ex b_{1} being Element of (Polynom-Ring R) st

( not b_{1} is zero & b_{1} is constant )

ex b_{1} being Element of the carrier of (Polynom-Ring R) st

( not b_{1} is zero & b_{1} is constant )

end;
cluster non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable constant for Element of (Polynom-Ring R);

existence ex b

( not b

proof end;

cluster V1() V4( NAT ) V5( the carrier of R) Function-like non empty total quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non zero constant for of ;

existence ex b

( not b

proof end;

registration

let R be domRing;

not for b_{1} being Element of (Polynom-Ring R) holds b_{1} is constant

not for b_{1} being Element of the carrier of (Polynom-Ring R) holds b_{1} is constant

end;
cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non constant for Element of (Polynom-Ring R);

existence not for b

proof end;

cluster V1() V4( NAT ) V5( the carrier of R) Function-like non empty total quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non constant for of ;

existence not for b

proof end;

definition
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);

for L being non empty ZeroStr

for a being Element of L holds a | L = (0_. L) +* (0,a);

registration
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
end;

registration

let L be non trivial ZeroStr ;

let a be non zero Element of L;

coherence

not a | L is zero

end;
let a be non zero Element of L;

coherence

not a | L is zero

proof end;

registration

let L be non trivial ZeroStr ;

ex b_{1} being Polynomial of L st

( not b_{1} is zero & b_{1} is constant )

end;
cluster V1() V4( NAT ) V5( the carrier of L) Function-like non empty total quasi_total finite-Support non zero constant for Polynomial of ;

existence ex b

( not b

proof end;

registration
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 (Polynom-Ring L) holds

( ( not p is zero & p is constant ) iff deg p = 0 )

for p being Element of the carrier of (Polynom-Ring L) 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)

for a being Element of L holds a | L = a * (1_. L)

proof end;

theorem T11: :: RING_4:20

for R being Ring

for p being Element of the carrier of (Polynom-Ring R) holds

( p is constant iff ex a being Element of R st p = a | R )

for p being Element of the carrier of (Polynom-Ring R) holds

( p is constant iff ex a being Element of R st p = a | R )

proof end;

notation
end;

registration

let L be non degenerated doubleLoopStr ;

coherence

1_. L is monic

not 0_. L is monic

end;
coherence

1_. L is monic

proof end;

coherence not 0_. L is monic

proof end;

registration

let L be non degenerated doubleLoopStr ;

ex b_{1} being Polynomial of L st b_{1} is monic

not for b_{1} being Polynomial of L holds b_{1} is monic

end;
cluster V1() V4( NAT ) V5( the carrier of L) Function-like non empty total quasi_total finite-Support monic for Polynomial of ;

existence ex b

proof end;

cluster V1() V4( NAT ) V5( the carrier of L) Function-like non empty total quasi_total finite-Support non monic for Polynomial of ;

existence not for b

proof end;

registration

let L be non degenerated right_complementable add-associative right_zeroed distributive doubleLoopStr ;

ex b_{1} being Element of the carrier of (Polynom-Ring L) st b_{1} is monic

not for b_{1} being Element of the carrier of (Polynom-Ring L) holds b_{1} is monic

end;
cluster V1() V4( NAT ) V5( the carrier of L) Function-like non empty total quasi_total left_add-cancelable right_add-cancelable add-cancelable right_complementable finite-Support monic for of ;

existence ex b

proof end;

cluster V1() V4( NAT ) V5( the carrier of L) Function-like non empty total quasi_total left_add-cancelable right_add-cancelable add-cancelable right_complementable finite-Support non monic for of ;

existence not for b

proof end;

registration

let L be non degenerated well-unital doubleLoopStr ;

let x be Element of L;

coherence

rpoly (1,x) is monic

end;
let x be Element of L;

coherence

rpoly (1,x) is monic

proof end;

definition

let L be Field;

let p be Element of the carrier of (Polynom-Ring L);

:: original: NormPolynomial

redefine func NormPolynomial p -> Element of the carrier of (Polynom-Ring L);

coherence

NormPolynomial p is Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 10;

end;
let p be Element of the carrier of (Polynom-Ring L);

:: original: NormPolynomial

redefine func NormPolynomial p -> Element of the carrier of (Polynom-Ring L);

coherence

NormPolynomial p is Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 10;

registration
end;

registration

let L be Field;

let p be non zero Element of the carrier of (Polynom-Ring L);

coherence

NormPolynomial p is monic ;

end;
let p be non zero Element of the carrier of (Polynom-Ring L);

coherence

NormPolynomial p is monic ;

theorem npl: :: RING_4:23

for F being Field

for p being non zero Element of the carrier of (Polynom-Ring F) holds NormPolynomial p = ((LC p) ") * p

for p being non zero Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) holds

( p is monic iff NormPolynomial p = p )

for p being non zero Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) holds

( q divides p iff NormPolynomial q divides p )

for p, q being Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) holds

( q divides p iff q divides NormPolynomial p )

for p, q being Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) holds NormPolynomial p is_associated_to p

for p being Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) holds

( NormPolynomial p is irreducible iff p is irreducible )

for p being Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring R) st p is_associated_to q holds

deg p = deg q

for p, q being Element of the carrier of (Polynom-Ring R) 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 (Polynom-Ring R) holds

( p is_associated_to q iff p = q )

for p, q being monic Element of the carrier of (Polynom-Ring R) holds

( p is_associated_to q iff p = q )

proof end;

definition

let R be Ring;

ex b_{1} being Function of R,(Polynom-Ring R) st

for x being Element of R holds b_{1} . x = x | R

for b_{1}, b_{2} being Function of R,(Polynom-Ring R) st ( for x being Element of R holds b_{1} . x = x | R ) & ( for x being Element of R holds b_{2} . x = x | R ) holds

b_{1} = b_{2}

end;
func canHom R -> Function of R,(Polynom-Ring R) means :defcanhom: :: RING_4:def 6

for x being Element of R holds it . x = x | R;

existence for x being Element of R holds it . x = x | R;

ex b

for x being Element of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defcanhom defines canHom RING_4:def 6 :

for R being Ring

for b_{2} being Function of R,(Polynom-Ring R) holds

( b_{2} = canHom R iff for x being Element of R holds b_{2} . x = x | R );

for R being Ring

for b

( b

registration

let R be Ring;

coherence

( canHom R is additive & canHom R is multiplicative & canHom R is unity-preserving )

end;
coherence

( canHom R is additive & canHom R is multiplicative & canHom R is unity-preserving )

proof end;

registration
end;

registration

let R be Ring;

coherence

( Polynom-Ring R is R -homomorphic & Polynom-Ring R is R -monomorphic )

end;
coherence

( Polynom-Ring R is R -homomorphic & Polynom-Ring R is R -monomorphic )

proof end;

registration

for b_{1} being 0 -characteristic Ring holds b_{1} is infinite
end;

cluster non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 0 -characteristic -> infinite 0 -characteristic for Ring;

coherence for b

proof end;

registration

let n be non trivial Nat;

ex b_{1} being Ring st

( b_{1} is n -characteristic & b_{1} is infinite )

end;
cluster non empty infinite left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Abelian add-associative right_zeroed V123() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative V249() V250() V251() V252() INT.Ring -homomorphic INT.Ring -homomorphic n -characteristic for Ring;

existence ex b

( b

proof end;

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

proof end;

registration

not for b_{1} being domRing holds b_{1} is almost_left_invertible
end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable non almost_left_invertible Abelian add-associative right_zeroed V123() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V249() V250() V251() V252() INT.Ring -homomorphic for domRing;

existence not for b

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

not for b_{1} being NonUnit of R holds b_{1} is zero

end;
cluster non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non unital for NonUnit of ;

existence not for b

proof end;

theorem :: RING_4:34

theorem Th90: :: RING_4:35

for R being domRing

for a being Element of R holds

( a | R is Unit of (Polynom-Ring R) iff a is Unit of R )

for a being Element of R holds

( a | R is Unit of (Polynom-Ring R) 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 (Polynom-Ring F) st p is Unit of (Polynom-Ring F) holds

deg p = 0

for p being Element of the carrier of (Polynom-Ring F) st p is Unit of (Polynom-Ring F) holds

deg p = 0

proof end;

theorem T8: :: RING_4:37

for F being Field

for p being Element of the carrier of (Polynom-Ring F) holds

( p is Unit of (Polynom-Ring F) iff deg p = 0 )

for p being Element of the carrier of (Polynom-Ring F) holds

( p is Unit of (Polynom-Ring F) iff deg p = 0 )

proof end;

theorem :: RING_4:38

for R being domRing

for p being Element of the carrier of (Polynom-Ring R) st p is Unit of (Polynom-Ring R) holds

( not p is zero & p is constant )

for p being Element of the carrier of (Polynom-Ring R) st p is Unit of (Polynom-Ring R) 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 (Polynom-Ring F) holds

( p is Unit of (Polynom-Ring F) iff ( not p is zero & p is constant ) )

for p being Element of the carrier of (Polynom-Ring F) holds

( p is Unit of (Polynom-Ring F) iff ( not p is zero & p is constant ) )

proof end;

registration

let R be domRing;

coherence

for b_{1} being Element of (Polynom-Ring R) st not b_{1} is constant holds

( not b_{1} is zero & not b_{1} is unital )

end;
coherence

for b

( not b

proof end;

registration

let F be domRing;

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F) st not b_{1} is constant holds

( not b_{1} is zero & not b_{1} is unital )

end;
coherence

for b

( not b

proof end;

registration

let F be Field;

coherence

for b_{1} being Element of (Polynom-Ring F) st not b_{1} is zero & b_{1} is constant holds

b_{1} is unital

for b_{1} being Element of (Polynom-Ring F) st b_{1} is unital holds

( not b_{1} is zero & b_{1} is constant )
;

end;
coherence

for b

b

proof end;

coherence for b

( not b

registration

let F be Field;

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F) st not b_{1} is zero & b_{1} is constant holds

b_{1} is unital

for b_{1} being Element of the carrier of (Polynom-Ring F) st b_{1} is unital holds

( not b_{1} is zero & b_{1} is constant )

end;
coherence

for b

b

proof end;

coherence for b

( not b

proof end;

theorem T88a: :: RING_4:40

for R being domRing

for p being Element of the carrier of (Polynom-Ring R) st ex q being Element of the carrier of (Polynom-Ring R) st

( q divides p & 1 <= deg q & deg q < deg p ) holds

p is reducible

for p being Element of the carrier of (Polynom-Ring R) st ex q being Element of the carrier of (Polynom-Ring R) 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 (Polynom-Ring F) holds

( ( p = 0_. F or p is Unit of (Polynom-Ring F) or ex q being Element of the carrier of (Polynom-Ring F) st

( q divides p & 1 <= deg q & deg q < deg p ) ) iff p is reducible )

for p being Element of the carrier of (Polynom-Ring F) holds

( ( p = 0_. F or p is Unit of (Polynom-Ring F) or ex q being Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring R) st deg p = 1 holds

p is irreducible

for p being monic Element of the carrier of (Polynom-Ring R) st deg p = 1 holds

p is irreducible

proof end;

theorem :: RING_4:43

ex p being non monic Element of the carrier of (Polynom-Ring INT.Ring) st

( deg p = 1 & p is reducible )

( 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 (Polynom-Ring F) st deg p = 1 holds

p is irreducible

for p being Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) holds

( p is irreducible iff deg p = 1 )

for p being Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) holds

( p is irreducible iff deg p = 1 ) )

( F is algebraic-closed iff for p being monic Element of the carrier of (Polynom-Ring F) holds

( p is irreducible iff deg p = 1 ) )

proof end;

registration

let R be domRing;

ex b_{1} being Element of (Polynom-Ring R) st b_{1} is irreducible

end;
cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable irreducible for Element of (Polynom-Ring R);

existence ex b

proof end;

registration

let R be domRing;

ex b_{1} being Element of the carrier of (Polynom-Ring R) st b_{1} is irreducible

end;
cluster V1() V4( NAT ) V5( the carrier of R) Function-like non empty total quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support irreducible for of ;

existence ex b

proof end;

registration

let R be Ring;

ex b_{1} being Element of (Polynom-Ring R) st b_{1} is reducible

end;
cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable reducible for Element of (Polynom-Ring R);

existence ex b

proof end;

registration

let R be Ring;

ex b_{1} being Element of the carrier of (Polynom-Ring R) st b_{1} is reducible

end;
cluster V1() V4( NAT ) V5( the carrier of R) Function-like non empty total quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support reducible for of ;

existence ex b

proof end;

registration

let F be Field;

coherence

for b_{1} being Element of (Polynom-Ring F) st b_{1} is constant holds

b_{1} is reducible
;

end;
coherence

for b

b

registration

let F be Field;

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F) st b_{1} is constant holds

b_{1} is reducible
;

end;
coherence

for b

b

registration

let F be Field;

coherence

for b_{1} being Element of (Polynom-Ring F) st b_{1} is irreducible holds

not b_{1} is constant
;

end;
coherence

for b

not b

registration

let F be Field;

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F) st b_{1} is irreducible holds

not b_{1} is constant
;

end;
coherence

for b

not b

registration

let F be Field;

let p be Element of the carrier of (Polynom-Ring F);

( (Polynom-Ring F) / ({p} -Ideal) is Abelian & (Polynom-Ring F) / ({p} -Ideal) is add-associative & (Polynom-Ring F) / ({p} -Ideal) is right_zeroed & (Polynom-Ring F) / ({p} -Ideal) is right_complementable & (Polynom-Ring F) / ({p} -Ideal) is commutative & (Polynom-Ring F) / ({p} -Ideal) is associative & (Polynom-Ring F) / ({p} -Ideal) is well-unital & (Polynom-Ring F) / ({p} -Ideal) is distributive ) ;

end;
let p be Element of the carrier of (Polynom-Ring F);

cluster (Polynom-Ring F) / ({p} -Ideal) -> right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative ;

coherence ( (Polynom-Ring F) / ({p} -Ideal) is Abelian & (Polynom-Ring F) / ({p} -Ideal) is add-associative & (Polynom-Ring F) / ({p} -Ideal) is right_zeroed & (Polynom-Ring F) / ({p} -Ideal) is right_complementable & (Polynom-Ring F) / ({p} -Ideal) is commutative & (Polynom-Ring F) / ({p} -Ideal) is associative & (Polynom-Ring F) / ({p} -Ideal) is well-unital & (Polynom-Ring F) / ({p} -Ideal) is distributive ) ;

registration

let F be Field;

let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

( not (Polynom-Ring F) / ({p} -Ideal) is degenerated & (Polynom-Ring F) / ({p} -Ideal) is almost_left_invertible ) by RING_2:26, RING_1:21;

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

( not (Polynom-Ring F) / ({p} -Ideal) is degenerated & (Polynom-Ring F) / ({p} -Ideal) is almost_left_invertible ) by RING_2:26, RING_1:21;

definition

let F be Field;

let p be Polynomial of F;

ex b_{1} being BinOp of (Polynom-Ring F) st

for r, q being Polynomial of F holds b_{1} . (r,q) = (r *' q) mod p

for b_{1}, b_{2} being BinOp of (Polynom-Ring F) st ( for r, q being Polynomial of F holds b_{1} . (r,q) = (r *' q) mod p ) & ( for r, q being Polynomial of F holds b_{2} . (r,q) = (r *' q) mod p ) holds

b_{1} = b_{2}

end;
let p be Polynomial of F;

func poly_mult_mod p -> BinOp of (Polynom-Ring F) means :defpmm: :: RING_4:def 7

for r, q being Polynomial of F holds it . (r,q) = (r *' q) mod p;

existence for r, q being Polynomial of F holds it . (r,q) = (r *' q) mod p;

ex b

for r, q being Polynomial of F holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defpmm defines poly_mult_mod RING_4:def 7 :

for F being Field

for p being Polynomial of F

for b_{3} being BinOp of (Polynom-Ring F) holds

( b_{3} = poly_mult_mod p iff for r, q being Polynomial of F holds b_{3} . (r,q) = (r *' q) mod p );

for F being Field

for p being Polynomial of F

for b

( b

pr1: for F being Field

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

proof end;

pr2: for F being Field

for p being non constant Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) 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 (Polynom-Ring F) 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 (Polynom-Ring F);

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = { q where q is Polynomial of F : deg q < deg p } & the addF of b_{1} = the addF of (Polynom-Ring F) || the carrier of b_{1} & the multF of b_{1} = (poly_mult_mod p) || the carrier of b_{1} & the OneF of b_{1} = 1_. F & the ZeroF of b_{1} = 0_. F )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = { q where q is Polynomial of F : deg q < deg p } & the addF of b_{1} = the addF of (Polynom-Ring F) || the carrier of b_{1} & the multF of b_{1} = (poly_mult_mod p) || the carrier of b_{1} & the OneF of b_{1} = 1_. F & the ZeroF of b_{1} = 0_. F & the carrier of b_{2} = { q where q is Polynomial of F : deg q < deg p } & the addF of b_{2} = the addF of (Polynom-Ring F) || the carrier of b_{2} & the multF of b_{2} = (poly_mult_mod p) || the carrier of b_{2} & the OneF of b_{2} = 1_. F & the ZeroF of b_{2} = 0_. F holds

b_{1} = b_{2}
;

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

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 (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 );

existence ( 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 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defprfp defines Polynom-Ring RING_4:def 8 :

for F being Field

for p being non constant Element of the carrier of (Polynom-Ring F)

for b_{3} being strict doubleLoopStr holds

( b_{3} = Polynom-Ring p iff ( the carrier of b_{3} = { q where q is Polynomial of F : deg q < deg p } & the addF of b_{3} = the addF of (Polynom-Ring F) || the carrier of b_{3} & the multF of b_{3} = (poly_mult_mod p) || the carrier of b_{3} & the OneF of b_{3} = 1_. F & the ZeroF of b_{3} = 0_. F ) );

for F being Field

for p being non constant Element of the carrier of (Polynom-Ring F)

for b

( b

registration

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

not Polynom-Ring p is degenerated

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

not Polynom-Ring p is degenerated

proof end;

registration

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

( Polynom-Ring p is Abelian & Polynom-Ring p is add-associative & Polynom-Ring p is right_zeroed & Polynom-Ring p is right_complementable )

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

( Polynom-Ring p is Abelian & Polynom-Ring p is add-associative & Polynom-Ring p is right_zeroed & Polynom-Ring p is right_complementable )

proof end;

registration

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

( Polynom-Ring p is associative & Polynom-Ring p is well-unital & Polynom-Ring p is distributive )

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

( Polynom-Ring p is associative & Polynom-Ring p is well-unital & Polynom-Ring p is distributive )

proof end;

definition

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

ex b_{1} being Function of (Polynom-Ring F),(Polynom-Ring p) st

for q being Polynomial of F holds b_{1} . q = q mod p

for b_{1}, b_{2} being Function of (Polynom-Ring F),(Polynom-Ring p) st ( for q being Polynomial of F holds b_{1} . q = q mod p ) & ( for q being Polynomial of F holds b_{2} . q = q mod p ) holds

b_{1} = b_{2}

end;
let 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 :dpm: :: RING_4:def 9

for q being Polynomial of F holds it . q = q mod p;

existence for q being Polynomial of F holds it . q = q mod p;

ex b

for q being Polynomial of F holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem dpm defines poly_mod RING_4:def 9 :

for F being Field

for p being non constant Element of the carrier of (Polynom-Ring F)

for b_{3} being Function of (Polynom-Ring F),(Polynom-Ring p) holds

( b_{3} = poly_mod p iff for q being Polynomial of F holds b_{3} . q = q mod p );

for F being Field

for p being non constant Element of the carrier of (Polynom-Ring F)

for b

( b

registration

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

( poly_mod p is additive & poly_mod p is multiplicative & poly_mod p is unity-preserving )

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

( poly_mod p is additive & poly_mod p is multiplicative & poly_mod p is unity-preserving )

proof end;

registration

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

Polynom-Ring p is Polynom-Ring F -homomorphic

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

Polynom-Ring p is Polynom-Ring F -homomorphic

proof end;

registration

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

poly_mod p is onto

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

poly_mod p is onto

proof end;

lemminuspoly: for R being Ring

for a being Element of (Polynom-Ring R)

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 (Polynom-Ring F) holds ker (poly_mod p) = {p} -Ideal

for p being non constant Element of the carrier of (Polynom-Ring F) holds ker (poly_mod p) = {p} -Ideal

proof end;

theorem ISO: :: RING_4:48

for F being Field

for p being non constant Element of the carrier of (Polynom-Ring F) holds (Polynom-Ring F) / ({p} -Ideal), Polynom-Ring p are_isomorphic

for p being non constant Element of the carrier of (Polynom-Ring F) holds (Polynom-Ring F) / ({p} -Ideal), Polynom-Ring p are_isomorphic

proof end;

registration

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

Polynom-Ring p is commutative

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

Polynom-Ring p is commutative

proof end;

registration

let F be Field;

let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

Polynom-Ring p is almost_left_invertible

end;
let p be irreducible Element of the carrier of (Polynom-Ring F);

coherence

Polynom-Ring p is almost_left_invertible

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

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;

ex b_{1} being Element of L st b_{1} is x,y -gcd

end;
let x, y be Element of L;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable x,y -gcd for Element of L;

existence ex b

proof end;

definition
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

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;

coherence

for b_{1} being Element of L st b_{1} is x,y -gcd holds

b_{1} is y,x -gcd
;

end;
let x, y be Element of L;

coherence

for b

b

definition

let F be Field;

let p, q be Element of the carrier of (Polynom-Ring F);

( ( p = 0_. F & q = 0_. F implies ex b_{1} being Element of the carrier of (Polynom-Ring F) st b_{1} = 0_. F ) & ( ( not p = 0_. F or not q = 0_. F ) implies ex b_{1} being Element of the carrier of (Polynom-Ring F) st

( b_{1} is a_gcd of p,q & b_{1} is monic ) ) )

for b_{1}, b_{2} being Element of the carrier of (Polynom-Ring F) holds

( ( p = 0_. F & q = 0_. F & b_{1} = 0_. F & b_{2} = 0_. F implies b_{1} = b_{2} ) & ( ( not p = 0_. F or not q = 0_. F ) & b_{1} is a_gcd of p,q & b_{1} is monic & b_{2} is a_gcd of p,q & b_{2} is monic implies b_{1} = b_{2} ) )

for b_{1} being Element of the carrier of (Polynom-Ring F) holds verum
;

end;
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 :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 it = 0_. F if ( p = 0_. F & q = 0_. F )

otherwise ( it is a_gcd of p,q & it is monic );

( ( p = 0_. F & q = 0_. F implies ex b

( b

proof end;

uniqueness for b

( ( p = 0_. F & q = 0_. F & b

proof end;

consistency for b

:: deftheorem dpg defines gcd RING_4:def 11 :

for F being Field

for p, q, b_{4} being Element of the carrier of (Polynom-Ring F) holds

( ( p = 0_. F & q = 0_. F implies ( b_{4} = p gcd q iff b_{4} = 0_. F ) ) & ( ( not p = 0_. F or not q = 0_. F ) implies ( b_{4} = p gcd q iff ( b_{4} is a_gcd of p,q & b_{4} is monic ) ) ) );

for F being Field

for p, q, b

( ( p = 0_. F & q = 0_. F implies ( b

definition

let F be Field;

let p, q be Element of the carrier of (Polynom-Ring F);

:: original: gcd

redefine func p gcd q -> Element of the carrier of (Polynom-Ring F);

commutativity

for p, q being Element of the carrier of (Polynom-Ring F) holds p gcd q = q gcd p

end;
let p, q be Element of the carrier of (Polynom-Ring F);

:: original: gcd

redefine func p gcd q -> Element of the carrier of (Polynom-Ring F);

commutativity

for p, q being Element of the carrier of (Polynom-Ring F) holds p gcd q = q gcd p

proof end;

definition

let F be Field;

let p, q be Element of (Polynom-Ring F);

:: original: gcd

redefine func p gcd q -> Element of the carrier of (Polynom-Ring F);

commutativity

for p, q being Element of (Polynom-Ring F) holds p gcd q = q gcd p

end;
let p, q be Element of (Polynom-Ring F);

:: original: gcd

redefine func p gcd q -> Element of the carrier of (Polynom-Ring F);

commutativity

for p, q being Element of (Polynom-Ring F) holds p gcd q = q gcd p

proof end;

registration

let F be Field;

let p, q be Element of the carrier of (Polynom-Ring F);

coherence

p gcd q is p,q -gcd

end;
let p, q be Element of the carrier of (Polynom-Ring F);

coherence

p gcd q is p,q -gcd

proof end;

registration
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);

coherence

( not p gcd q is zero & p gcd q is monic )

end;
let p be Element of the carrier of (Polynom-Ring F);

let q be non zero Element of the carrier of (Polynom-Ring F);

coherence

( not p gcd q is zero & p gcd q is monic )

proof end;

registration

let F be Field;

let p be Element of (Polynom-Ring F);

let q be non zero Element of (Polynom-Ring F);

coherence

( not p gcd q is zero & p gcd q is monic )

end;
let p be Element of (Polynom-Ring F);

let q be non zero Element of (Polynom-Ring F);

coherence

( not p gcd q is zero & p gcd q is monic )

proof end;

registration

let F be Field;

let p, q be zero Element of the carrier of (Polynom-Ring F);

coherence

p gcd q is zero

end;
let p, q be zero Element of the carrier of (Polynom-Ring F);

coherence

p gcd q is zero

proof end;

registration
end;

theorem :: RING_4:50

for F being Field

for 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 ) )

for 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 ) )

proof end;

theorem :: RING_4:51

definition

let F be Field;

let p, q be Polynomial of F;

ex b_{1} being Polynomial of F ex a, b being Element of (Polynom-Ring F) st

( a = p & b = q & b_{1} = a gcd b )

for b_{1}, b_{2} being Polynomial of F st ex a, b being Element of (Polynom-Ring F) st

( a = p & b = q & b_{1} = a gcd b ) & ex a, b being Element of (Polynom-Ring F) st

( a = p & b = q & b_{2} = a gcd b ) holds

b_{1} = b_{2}
;

end;
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 (Polynom-Ring F) st

( a = p & b = q & it = a gcd b );

existence ex a, b being Element of (Polynom-Ring F) st

( a = p & b = q & it = a gcd b );

ex b

( a = p & b = q & b

proof end;

uniqueness for b

( a = p & b = q & b

( a = p & b = q & b

b

:: deftheorem dd defines gcd RING_4:def 12 :

for F being Field

for p, q, b_{4} being Polynomial of F holds

( b_{4} = p gcd q iff ex a, b being Element of (Polynom-Ring F) st

( a = p & b = q & b_{4} = a gcd b ) );

for F being Field

for p, q, b

( b

( a = p & b = q & 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

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

registration

let F be Field;

let p be Polynomial of F;

let q be non zero Polynomial of F;

coherence

( not p gcd q is zero & p gcd q is monic )

end;
let p be Polynomial of F;

let q be non zero Polynomial of F;

coherence

( not p gcd q is zero & p gcd q is monic )

proof end;

registration
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 ) )

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 ) ) )

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;