:: Some Algebraic Properties of Polynomial Rings
:: by Christoph Schwarzweller , Artur Korni{\l}owicz and Agnieszka Rowinska-Schwarzweller
::
:: Received June 30, 2016
:: 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

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

coherence
for b₁ being Ring st b₁ is almost_left_invertible & b₁ is commutative holds
b₁ is almost_right_invertible

proof end;

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

coherence
for b₁ being Ring st b₁ is almost_right_invertible & b₁ is commutative holds
b₁ is almost_left_invertible

proof end;

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

coherence
for b₁ being Ring st b₁ is almost_left_cancelable & b₁ is commutative holds
b₁ is almost_right_cancelable

proof end;

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

coherence
for b₁ being Ring st b₁ is almost_right_cancelable & b₁ is commutative holds
b₁ 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 ;

cluster non empty L -polynomial-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is L -polynomial-membered )

proof end;

end;

registration

let L be non empty ZeroStr ;

cluster non empty L -polynomial-membered for 1-sorted ;

existence
ex b₁ being 1-sorted st
( not b₁ is empty & b₁ 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

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

cluster Polynom-Ring L -> L -polynomial-membered ;

coherence
Polynom-Ring L is L -polynomial-membered

proof end;

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₁ being Element of X holds b₁ 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 (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;

registration

let R be Ring;

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 Element of the carrier of (Polynom-Ring R);

existence
ex b₁ being Element of the carrier of (Polynom-Ring R) st b₁ is zero

proof end;

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

existence
ex b₁ being Element of (Polynom-Ring R) st b₁ 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 b₁ being Polynomial of R st b₁ is zero

proof end;

end;

registration

let R be non degenerated Ring;

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 Element of the carrier of (Polynom-Ring R);

existence
not for b₁ being Element of the carrier of (Polynom-Ring R) holds b₁ is zero

proof end;

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

existence
not for b₁ being Element of (Polynom-Ring R) holds b₁ 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 (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;

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

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

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

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

cluster Polynom-Ring L -> well-unital ;

coherence
Polynom-Ring L is well-unital

proof end;

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

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 (Polynom-Ring R) holds
( x is constant iff deg x <= 0 );

registration

let R be non degenerated Ring;

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

existence
ex b₁ being Element of (Polynom-Ring R) st
( not b₁ is zero & b₁ is constant )

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 Element of the carrier of (Polynom-Ring R);

existence
ex b₁ being Element of the carrier of (Polynom-Ring R) st
( not b₁ is zero & b₁ is constant )

proof end;

end;

registration

let R be domRing;

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

existence
not for b₁ being Element of (Polynom-Ring R) holds b₁ is constant

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 Element of the carrier of (Polynom-Ring R);

existence
not for b₁ being Element of the carrier of (Polynom-Ring R) holds b₁ 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;

cluster a | L -> finite-Support ;

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 b₁ being Polynomial of L st
( not b₁ is zero & b₁ 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 (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)

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 (Polynom-Ring R) 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 b₁ being Polynomial of L st b₁ 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 b₁ being Polynomial of L holds b₁ is monic

proof end;

end;

registration

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

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

existence
ex b₁ being Element of the carrier of (Polynom-Ring L) st b₁ is monic

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

existence
not for b₁ being Element of the carrier of (Polynom-Ring L) holds b₁ 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 (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;

registration

let F be Field;
let p be non zero Polynomial of F;

cluster NormPolynomial p -> monic ;

coherence
NormPolynomial p is monic ;

end;

registration

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

cluster NormPolynomial p -> monic ;

coherence
NormPolynomial p is monic ;

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

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 )

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 )

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

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 )

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

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 )

proof end;

definition

let R be Ring;

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
ex b₁ being Function of R,(Polynom-Ring R) st
for x being Element of R holds b₁ . x = x | R

proof end;

uniqueness
for b₁, b₂ being Function of R,(Polynom-Ring R) st ( for x being Element of R holds b₁ . x = x | R ) & ( for x being Element of R holds b₂ . x = x | R ) holds
b₁ = b₂

proof end;

end;

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

registration

let R be Ring;

cluster canHom R -> additive unity-preserving multiplicative ;

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

proof end;

end;

registration

let R be Ring;

cluster canHom R -> monomorphism ;

coherence
canHom R is RingMonomorphism

proof end;

end;

registration

let R be Ring;

cluster Polynom-Ring R -> R -homomorphic R -monomorphic ;

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

proof end;

end;

theorem :: RING_4:31

for R being Ring holds Char (Polynom-Ring R) = Char R by RING_3:88;

registration

let R be non degenerated Ring;

cluster Polynom-Ring R -> infinite ;

coherence
not Polynom-Ring R is finite

proof end;

end;

registration

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

coherence
for b₁ being 0 -characteristic Ring holds b₁ 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;

cluster Polynom-Ring (Z/ n) -> infinite ;

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;

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 V251() V252() V253() V254() INT.Ring -homomorphic INT.Ring -homomorphic n -characteristic for doubleLoopStr ;

existence
ex b₁ being Ring st
( b₁ is n -characteristic & b₁ is infinite )

proof end;

end;

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

proof end;

registration

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 V251() V252() V253() V254() INT.Ring -homomorphic for doubleLoopStr ;

existence
not for b₁ being domRing holds b₁ 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;

cluster non zero left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non unital for Element of the carrier of R;

existence
not for b₁ being NonUnit of R holds b₁ is zero

proof end;

end;

registration

cluster INT.Ring -> non almost_left_invertible ;

coherence
not INT.Ring is almost_left_invertible

proof end;

end;

registration

let R be domRing;

cluster Polynom-Ring R -> non almost_left_invertible ;

coherence
not Polynom-Ring R is almost_left_invertible 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 (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

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 )

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 )

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

proof end;

registration

let R be domRing;

cluster non constant -> non zero non unital for Element of the carrier of (Polynom-Ring R);

coherence
for b₁ being Element of (Polynom-Ring R) st not b₁ is constant holds
( not b₁ is zero & not b₁ is unital )

proof end;

end;

registration

let F be domRing;

cluster non constant -> non zero non unital for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of the carrier of (Polynom-Ring F) st not b₁ is constant holds
( not b₁ is zero & not b₁ is unital )

proof end;

end;

registration

let F be Field;

cluster non zero constant -> unital for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of (Polynom-Ring F) st not b₁ is zero & b₁ is constant holds
b₁ is unital

proof end;

cluster unital -> non zero constant for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of (Polynom-Ring F) st b₁ is unital holds
( not b₁ is zero & b₁ is constant ) ;

end;

registration

let F be Field;

cluster non zero constant -> unital for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of the carrier of (Polynom-Ring F) st not b₁ is zero & b₁ is constant holds
b₁ is unital

proof end;

cluster unital -> non zero constant for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of the carrier of (Polynom-Ring F) st b₁ is unital holds
( not b₁ is zero & b₁ is constant )

proof end;

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

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 )

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

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 )

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

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 )

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

proof end;

registration

let R be domRing;

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

existence
ex b₁ being Element of (Polynom-Ring R) st b₁ is irreducible

proof end;

end;

registration

let R be domRing;

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 Element of the carrier of (Polynom-Ring R);

existence
ex b₁ being Element of the carrier of (Polynom-Ring R) st b₁ is irreducible

proof end;

end;

registration

let R be Ring;

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

existence
ex b₁ being Element of (Polynom-Ring R) st b₁ is reducible

proof end;

end;

registration

let R be Ring;

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 Element of the carrier of (Polynom-Ring R);

existence
ex b₁ being Element of the carrier of (Polynom-Ring R) st b₁ is reducible

proof end;

end;

registration

let R be domRing;

cluster IRR (Polynom-Ring R) -> non empty ;

coherence
not IRR (Polynom-Ring R) is empty

proof end;

end;

registration

let F be Field;

cluster constant -> reducible for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of (Polynom-Ring F) st b₁ is constant holds
b₁ is reducible ;

end;

registration

let F be Field;

cluster constant -> reducible for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of the carrier of (Polynom-Ring F) st b₁ is constant holds
b₁ is reducible ;

end;

registration

let F be Field;

cluster irreducible -> non constant for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of (Polynom-Ring F) st b₁ is irreducible holds
not b₁ is constant ;

end;

registration

let F be Field;

cluster irreducible -> non constant for Element of the carrier of (Polynom-Ring F);

coherence
for b₁ being Element of the carrier of (Polynom-Ring F) st b₁ is irreducible holds
not b₁ is constant ;

end;

registration

let F be Field;
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 ) ;

end;

registration

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

cluster (Polynom-Ring F) / ({p} -Ideal) -> non degenerated almost_left_invertible ;

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;

definition

let F be Field;
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
ex b₁ being BinOp of (Polynom-Ring F) st
for r, q being Polynomial of F holds b₁ . (r,q) = (r *' q) mod p

proof end;

uniqueness
for b₁, b₂ being BinOp of (Polynom-Ring F) st ( for r, q being Polynomial of F holds b₁ . (r,q) = (r *' q) mod p ) & ( for r, q being Polynomial of F holds b₂ . (r,q) = (r *' q) mod p ) holds
b₁ = b₂

proof end;

end;

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

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

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
ex b₁ being strict doubleLoopStr st
( the carrier of b₁ = { q where q is Polynomial of F : deg q < deg p } & the addF of b₁ = the addF of (Polynom-Ring F) || the carrier of b₁ & the multF of b₁ = (poly_mult_mod p) || the carrier of b₁ & the OneF of b₁ = 1_. F & the ZeroF of b₁ = 0_. F )

proof end;

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

end;

:: 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₃ being strict doubleLoopStr holds
( b₃ = Polynom-Ring p iff ( the carrier of b₃ = { q where q is Polynomial of F : deg q < deg p } & the addF of b₃ = the addF of (Polynom-Ring F) || the carrier of b₃ & the multF of b₃ = (poly_mult_mod p) || the carrier of b₃ & the OneF of b₃ = 1_. F & the ZeroF of b₃ = 0_. F ) );

registration

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

cluster Polynom-Ring p -> non degenerated strict ;

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

cluster Polynom-Ring p -> right_complementable strict Abelian add-associative right_zeroed ;

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;

end;

registration

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

cluster Polynom-Ring p -> strict well-unital distributive associative ;

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

proof end;

end;

definition

let F be Field;
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
ex b₁ being Function of (Polynom-Ring F),(Polynom-Ring p) st
for q being Polynomial of F holds b₁ . q = q mod p

proof end;

uniqueness
for b₁, b₂ being Function of (Polynom-Ring F),(Polynom-Ring p) st ( for q being Polynomial of F holds b₁ . q = q mod p ) & ( for q being Polynomial of F holds b₂ . q = q mod p ) holds
b₁ = b₂

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 (Polynom-Ring F)
for b₃ being Function of (Polynom-Ring F),(Polynom-Ring p) holds
( b₃ = poly_mod p iff for q being Polynomial of F holds b₃ . q = q mod p );

registration

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

cluster poly_mod p -> additive unity-preserving multiplicative ;

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

proof end;

end;

registration

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

cluster Polynom-Ring p -> strict Polynom-Ring F -homomorphic ;

coherence
Polynom-Ring p is Polynom-Ring F -homomorphic

proof end;

end;

registration

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

cluster poly_mod p -> onto ;

coherence
poly_mod p is onto

proof end;

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

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

proof end;

registration

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

cluster Polynom-Ring p -> strict commutative ;

coherence
Polynom-Ring p is commutative

proof end;

end;

registration

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

cluster Polynom-Ring p -> almost_left_invertible strict ;

coherence
Polynom-Ring p is almost_left_invertible

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;

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

existence
ex b₁ being Element of L st b₁ 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 b₁ being Element of L st b₁ is x,y -gcd holds
b₁ is y,x -gcd ;

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 :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 b₁ being Element of the carrier of (Polynom-Ring F) st b₁ = 0_. F ) & ( ( not p = 0_. F or not q = 0_. F ) implies ex b₁ being Element of the carrier of (Polynom-Ring F) st
( b₁ is a_gcd of p,q & b₁ is monic ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of the carrier of (Polynom-Ring F) holds
( ( p = 0_. F & q = 0_. F & b₁ = 0_. F & b₂ = 0_. F implies b₁ = b₂ ) & ( ( not p = 0_. F or not q = 0_. F ) & b₁ is a_gcd of p,q & b₁ is monic & b₂ is a_gcd of p,q & b₂ is monic implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Element of the carrier of (Polynom-Ring F) holds verum ;

end;

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

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

proof end;

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

proof end;

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 ;

coherence
p gcd q is p,q -gcd

proof end;

end;

registration

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

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 (Polynom-Ring F);
let q be non zero Element of the carrier of (Polynom-Ring 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 be Element of (Polynom-Ring F);
let q be non zero Element of (Polynom-Ring 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 Element of the carrier of (Polynom-Ring F);

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

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

for F being Field
for 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 ) ) 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 (Polynom-Ring F) st
( a = p & b = q & it = a gcd b );

existence
ex b₁ being Polynomial of F ex a, b being Element of (Polynom-Ring F) st
( a = p & b = q & b₁ = a gcd b )

proof end;

uniqueness
for b₁, b₂ being Polynomial of F st ex a, b being Element of (Polynom-Ring F) st
( a = p & b = q & b₁ = a gcd b ) & ex a, b being Element of (Polynom-Ring F) st
( a = p & b = q & b₂ = a gcd b ) holds
b₁ = b₂ ;

end;

:: deftheorem dd defines gcd RING_4:def 12 :
for F being Field
for p, q, b₄ being Polynomial of F holds
( b₄ = p gcd q iff ex a, b being Element of (Polynom-Ring F) st
( a = p & b = q & b₄ = 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;