:: by Christoph Schwarzweller

::

:: Received August 30, 2017

:: Copyright (c) 2017 Association of Mizar Users

registration

ex b_{1} being Nat st

( not b_{1} is trivial & not b_{1} is prime )
by NAT_2:def 1, INT_2:29;

end;

cluster non trivial epsilon-transitive epsilon-connected ordinal natural V31() integer dim-like finite cardinal ext-real non negative complex non prime for set ;

existence ex b

( not b

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

prl4: for R being Ring

for a being Element of R holds a |^ 2 = a * a

proof end;

registration

let R be non degenerated Ring;

for b_{1} being non zero Polynomial of R holds b_{1} is non-zero
;

for b_{1} being Polynomial of R st b_{1} is monic holds

not b_{1} is zero
;

end;
cluster Function-like V18( omega , the carrier of R) finite-Support non zero -> non zero for Element of K19(K20(omega, the carrier of R));

coherence for b

cluster Function-like V18( omega , the carrier of R) finite-Support monic -> non zero for Element of K19(K20(omega, the carrier of R));

coherence for b

not b

registration
end;

registration

let R be Ring;

let p be zero Polynomial of R;

let q be Polynomial of R;

coherence

p *' q is zero

q *' p is zero

end;
let p be zero Polynomial of R;

let q be Polynomial of R;

coherence

p *' q is zero

proof end;

coherence q *' p is zero

proof end;

registration

let R be Ring;

let p be zero Polynomial of R;

let q be Polynomial of R;

reducibility

p + q = q

q + p = q ;

end;
let p be zero Polynomial of R;

let q be Polynomial of R;

reducibility

p + q = q

proof end;

reducibility q + p = q ;

registration

let R be Ring;

let p be Polynomial of R;

reducibility

p *' (0_. R) = 0_. R by POLYNOM3:34;

reducibility

p *' (1_. R) = p by POLYNOM3:35;

reducibility

(0_. R) *' p = 0_. R by POLYNOM4:2;

reducibility

(1_. R) *' p = p by RING_4:12;

end;
let p be Polynomial of R;

reducibility

p *' (0_. R) = 0_. R by POLYNOM3:34;

reducibility

p *' (1_. R) = p by POLYNOM3:35;

reducibility

(0_. R) *' p = 0_. R by POLYNOM4:2;

reducibility

(1_. R) *' p = p by RING_4:12;

registration
end;

Th28: for L being non empty ZeroStr

for a being Element of L holds (a | L) . 0 = a

proof end;

Th25a: for R being domRing

for p being Polynomial of R

for a being non zero Element of R holds len (a * p) = len p

proof end;

theorem Th25: :: RING_5:4

for R being domRing

for p being Polynomial of R

for a being non zero Element of R holds deg (a * p) = deg p

for p being Polynomial of R

for a being non zero Element of R holds deg (a * p) = deg p

proof end;

theorem prl0a: :: RING_5:5

for R being domRing

for p being Polynomial of R

for a being Element of R holds LC (a * p) = a * (LC p)

for p being Polynomial of R

for a being Element of R holds LC (a * p) = a * (LC p)

proof end;

theorem Th30: :: RING_5:7

for R being domRing

for p being Polynomial of R

for v, x being Element of R holds eval ((v * p),x) = v * (eval (p,x))

for p being Polynomial of R

for v, x being Element of R holds eval ((v * p),x) = v * (eval (p,x))

proof end;

prl2: for R being non degenerated comRing

for p, q being Polynomial of R

for a being Element of R st a is_a_root_of p holds

a is_a_root_of p *' q

proof end;

registration
end;

registration

let R be domRing;

let a be Element of R;

let k be Nat;

coherence

( not (rpoly (1,a)) `^ k is zero & (rpoly (1,a)) `^ k is monic )

end;
let a be Element of R;

let k be Nat;

coherence

( not (rpoly (1,a)) `^ k is zero & (rpoly (1,a)) `^ k is monic )

proof end;

theorem lcrpol: :: RING_5:9

for R being non degenerated Ring

for a being Element of R

for k being non zero Element of NAT holds LC (rpoly (k,a)) = 1. R

for a being Element of R

for k being non zero Element of NAT holds LC (rpoly (k,a)) = 1. R

proof end;

theorem repr: :: RING_5:10

for R being non empty non degenerated well-unital doubleLoopStr

for a being Element of R holds <%(- a),(1. R)%> = rpoly (1,a)

for a being Element of R holds <%(- a),(1. R)%> = rpoly (1,a)

proof end;

theorem Th9: :: RING_5:11

for R being domRing

for p being Polynomial of R

for x being Element of R holds

( eval (p,x) = 0. R iff rpoly (1,x) divides p )

for p being Polynomial of R

for x being Element of R holds

( eval (p,x) = 0. R iff rpoly (1,x) divides p )

proof end;

theorem :: RING_5:12

for F being domRing

for p, q being Polynomial of F

for a being Element of F holds

( not rpoly (1,a) divides p *' q or rpoly (1,a) divides p or rpoly (1,a) divides q )

for p, q being Polynomial of F

for a being Element of F holds

( not rpoly (1,a) divides p *' q or rpoly (1,a) divides p or rpoly (1,a) divides q )

proof end;

theorem prl25: :: RING_5:13

for R being domRing

for p being Polynomial of R

for q being non zero Polynomial of R st p divides q holds

deg p <= deg q

for p being Polynomial of R

for q being non zero Polynomial of R st p divides q holds

deg p <= deg q

proof end;

theorem divi1: :: RING_5:14

for R being non degenerated comRing

for q being Polynomial of R

for p being non zero Polynomial of R

for b being non zero Element of R st q divides p holds

q divides b * p

for q being Polynomial of R

for p being non zero Polynomial of R

for b being non zero Element of R st q divides p holds

q divides b * p

proof end;

theorem :: RING_5:15

for F being Field

for q being Polynomial of F

for p being non zero Polynomial of F

for b being non zero Element of F holds

( q divides p iff q divides b * p )

for q being Polynomial of F

for p being non zero Polynomial of F

for b being non zero Element of F holds

( q divides p iff q divides b * p )

proof end;

theorem divi1b: :: RING_5:16

for R being domRing

for p being non zero Polynomial of R

for a being Element of R

for b being non zero Element of R holds

( rpoly (1,a) divides p iff rpoly (1,a) divides b * p )

for p being non zero Polynomial of R

for a being Element of R

for b being non zero Element of R holds

( rpoly (1,a) divides p iff rpoly (1,a) divides b * p )

proof end;

theorem divi1ad: :: RING_5:17

for n being Nat

for R being domRing

for p being non zero Polynomial of R

for a being Element of R

for b being non zero Element of R holds

( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )

for R being domRing

for p being non zero Polynomial of R

for a being Element of R

for b being non zero Element of R holds

( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )

proof end;

registration

let R be domRing;

let p be non zero Polynomial of R;

let b be non zero Element of R;

coherence

not b * p is zero

end;
let p be non zero Polynomial of R;

let b be non zero Element of R;

coherence

not b * p is zero

proof end;

registration

let R be non degenerated Ring;

let a be non zero Element of R;

coherence

not a | R is with_roots

end;
let a be non zero Element of R;

coherence

not a | R is with_roots

proof end;

registration

let R be non degenerated Ring;

for b_{1} being Polynomial of R st not b_{1} is zero & b_{1} is with_roots holds

not b_{1} is constant

end;
cluster Function-like V18( omega , the carrier of R) finite-Support non zero with_roots -> non constant for Element of K19(K20(omega, the carrier of R));

coherence for b

not b

proof end;

registration

let R be non degenerated Ring;

for b_{1} being Polynomial of R st not b_{1} is with_roots holds

not b_{1} is zero
;

end;
cluster Function-like V18( omega , the carrier of R) finite-Support non with_roots -> non zero for Element of K19(K20(omega, the carrier of R));

coherence for b

not b

registration

let R be non degenerated Ring;

let a be Element of R;

coherence

( not rpoly (1,a) is zero & rpoly (1,a) is with_roots ) by HURWITZ:30, POLYNOM5:def 8;

end;
let a be Element of R;

coherence

( not rpoly (1,a) is zero & rpoly (1,a) is with_roots ) by HURWITZ:30, POLYNOM5:def 8;

registration

let R be non degenerated Ring;

ex b_{1} being Polynomial of R st

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

ex b_{1} being Polynomial of R st

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

end;
cluster Relation-like omega -defined the carrier of R -valued Function-like V18( omega , the carrier of R) finite-Support non zero non with_roots for Element of K19(K20(omega, the carrier of R));

existence ex b

( not b

proof end;

cluster Relation-like omega -defined the carrier of R -valued Function-like V18( omega , the carrier of R) finite-Support non zero with_roots for Element of K19(K20(omega, the carrier of R));

existence ex b

( not b

proof end;

registration

let R be domRing;

let p be non with_roots Polynomial of R;

let a be non zero Element of R;

coherence

not a * p is with_roots

end;
let p be non with_roots Polynomial of R;

let a be non zero Element of R;

coherence

not a * p is with_roots

proof end;

registration

let R be domRing;

let p be with_roots Polynomial of R;

let a be Element of R;

coherence

a * p is with_roots

end;
let p be with_roots Polynomial of R;

let a be Element of R;

coherence

a * p is with_roots

proof end;

registration

let R be non degenerated comRing;

let p be with_roots Polynomial of R;

let q be Polynomial of R;

coherence

p *' q is with_roots

end;
let p be with_roots Polynomial of R;

let q be Polynomial of R;

coherence

p *' q is with_roots

proof end;

registration

let R be domRing;

let p, q be non with_roots Polynomial of R;

coherence

not p *' q is with_roots

end;
let p, q be non with_roots Polynomial of R;

coherence

not p *' q is with_roots

proof end;

registration

let R be non degenerated comRing;

let a be Element of R;

let k be non zero Element of NAT ;

coherence

( not rpoly (k,a) is constant & rpoly (k,a) is monic & rpoly (k,a) is with_roots )

end;
let a be Element of R;

let k be non zero Element of NAT ;

coherence

( not rpoly (k,a) is constant & rpoly (k,a) is monic & rpoly (k,a) is with_roots )

proof end;

registration

let R be non degenerated Ring;

ex b_{1} being Polynomial of R st

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

end;
cluster Relation-like omega -defined the carrier of R -valued Function-like V18( omega , the carrier of R) finite-Support non constant monic for Element of K19(K20(omega, the carrier of R));

existence ex b

( not b

proof end;

registration

let R be domRing;

let a be Element of R;

let k be non zero Nat;

let n be non zero Element of NAT ;

coherence

( not (rpoly (n,a)) `^ k is constant & (rpoly (n,a)) `^ k is monic & (rpoly (n,a)) `^ k is with_roots )

end;
let a be Element of R;

let k be non zero Nat;

let n be non zero Element of NAT ;

coherence

( not (rpoly (n,a)) `^ k is constant & (rpoly (n,a)) `^ k is monic & (rpoly (n,a)) `^ k is with_roots )

proof end;

registration
end;

registration

let R be non degenerated Ring;

let p be non with_roots Polynomial of R;

coherence

Roots p is empty

end;
let p be non with_roots Polynomial of R;

coherence

Roots p is empty

proof end;

registration

let R be domRing;

ex b_{1} being Polynomial of R st

( b_{1} is monic & b_{1} is with_roots )

ex b_{1} being Polynomial of R st

( b_{1} is monic & not b_{1} is with_roots )

end;
cluster Relation-like omega -defined the carrier of R -valued Function-like V18( omega , the carrier of R) finite-Support monic with_roots for Element of K19(K20(omega, the carrier of R));

existence ex b

( b

proof end;

cluster Relation-like omega -defined the carrier of R -valued Function-like V18( omega , the carrier of R) finite-Support monic non with_roots for Element of K19(K20(omega, the carrier of R));

existence ex b

( b

proof end;

theorem :: RING_5:19

for F being domRing

for p being Polynomial of F

for b being non zero Element of F holds Roots (b * p) = Roots p

for p being Polynomial of F

for b being non zero Element of F holds Roots (b * p) = Roots p

proof end;

degpol: for R being domRing

for p being non zero Polynomial of R ex n being natural number st

( n = card (Roots p) & n <= deg p )

proof end;

bbbag: for X being non empty set

for b being bag of X holds

( b is zero iff rng b = {0} )

proof end;

registration

let X be non empty set ;

ex b_{1} being bag of X st b_{1} is zero

not for b_{1} being bag of X holds b_{1} is zero

end;
cluster Relation-like X -defined RAT -valued Function-like non empty total V109() V110() V111() V112() finite-support zero for set ;

existence ex b

proof end;

cluster Relation-like X -defined RAT -valued Function-like non empty total V109() V110() V111() V112() finite-support non zero for set ;

existence not for b

proof end;

theorem :: RING_5:25

registration

let X be non empty set ;

let b1 be non zero bag of X;

let b2 be bag of X;

coherence

not b1 + b2 is zero

end;
let b1 be non zero bag of X;

let b2 be bag of X;

coherence

not b1 + b2 is zero

proof end;

theorem bb7a: :: RING_5:26

for X being non empty set

for b being bag of X

for x being Element of X st support b = {x} holds

b = ({x},(b . x)) -bag

for b being bag of X

for x being Element of X st support b = {x} holds

b = ({x},(b . x)) -bag

proof end;

theorem bb7: :: RING_5:27

for X being non empty set

for b being non empty bag of X

for x being Element of X holds

( support b = {x} iff ( b = ({x},(b . x)) -bag & b . x <> 0 ) )

for b being non empty bag of X

for x being Element of X holds

( support b = {x} iff ( b = ({x},(b . x)) -bag & b . x <> 0 ) )

proof end;

:: deftheorem defines Bag RING_5:def 1 :

for X being set

for S being finite Subset of X holds Bag S = (S,1) -bag ;

for X being set

for S being finite Subset of X holds Bag S = (S,1) -bag ;

registration

let X be non empty set ;

let S be non empty finite Subset of X;

coherence

not Bag S is zero

end;
let S be non empty finite Subset of X;

coherence

not Bag S is zero

proof end;

definition
end;

:: deftheorem defines \ RING_5:def 2 :

for X being non empty set

for b being bag of X

for a being Element of X holds b \ a = b +* (a,0);

for X being non empty set

for b being bag of X

for a being Element of X holds b \ a = b +* (a,0);

bb1: for X being non empty set

for b being bag of X

for a being Element of X holds (b \ a) . a = 0

proof end;

theorem :: RING_5:28

for X being non empty set

for b being bag of X

for a being Element of X holds

( b \ a = b iff not a in support b )

for b being bag of X

for a being Element of X holds

( b \ a = b iff not a in support b )

proof end;

theorem bb3a: :: RING_5:29

for X being non empty set

for b being bag of X

for a being Element of X holds support (b \ a) = (support b) \ {a}

for b being bag of X

for a being Element of X holds support (b \ a) = (support b) \ {a}

proof end;

theorem bb3: :: RING_5:30

for X being non empty set

for b being bag of X

for a being Element of X holds (b \ a) + (({a},(b . a)) -bag) = b

for b being bag of X

for a being Element of X holds (b \ a) + (({a},(b . a)) -bag) = b

proof end;

theorem bb4: :: RING_5:31

for X being non empty set

for a being Element of X

for n being Element of NAT holds card (({a},n) -bag) = n

for a being Element of X

for n being Element of NAT holds card (({a},n) -bag) = n

proof end;

registration

let R be domRing;

let p be non zero with_roots Polynomial of R;

coherence

not BRoots p is zero

end;
let p be non zero with_roots Polynomial of R;

coherence

not BRoots p is zero

proof end;

theorem multipp0: :: RING_5:32

for R being non degenerated comRing

for p being non zero Polynomial of R

for a being Element of R holds

( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )

for p being non zero Polynomial of R

for a being Element of R holds

( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )

proof end;

theorem multip: :: RING_5:33

for n being Nat

for R being domRing

for p being non zero Polynomial of R

for a being Element of R holds

( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )

for R being domRing

for p being non zero Polynomial of R

for a being Element of R holds

( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )

proof end;

theorem multip1d: :: RING_5:36

for R being domRing

for p being non zero Polynomial of R

for b being non zero Element of R

for a being Element of R holds multiplicity (p,a) = multiplicity ((b * p),a)

for p being non zero Polynomial of R

for b being non zero Element of R

for a being Element of R holds multiplicity (p,a) = multiplicity ((b * p),a)

proof end;

BR3: for R being domRing

for a being non zero Element of R holds support (BRoots (a | R)) = {}

proof end;

theorem llll: :: RING_5:37

for R being domRing

for p being non zero Polynomial of R

for b being non zero Element of R holds BRoots (b * p) = BRoots p

for p being non zero Polynomial of R

for b being non zero Element of R holds BRoots (b * p) = BRoots p

proof end;

theorem lemacf1: :: RING_5:38

for R being domRing

for p being non zero non with_roots Polynomial of R holds BRoots p = EmptyBag the carrier of R

for p being non zero non with_roots Polynomial of R holds BRoots p = EmptyBag the carrier of R

proof end;

theorem :: RING_5:41

for R being domRing

for p, q being non zero Polynomial of R holds card (BRoots (p *' q)) = (card (BRoots p)) + (card (BRoots q))

for p, q being non zero Polynomial of R holds card (BRoots (p *' q)) = (card (BRoots p)) + (card (BRoots q))

proof end;

Lm10: for n being Nat

for L being non empty unital doubleLoopStr holds

( ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . 0 = 1. L & ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = 1. L )

proof end;

Lm11: for L being non empty unital doubleLoopStr

for i, n being Nat st i <> 0 & i <> n holds

((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . i = 0. L

proof end;

definition

let R be non empty unital doubleLoopStr ;

let n be Nat;

coherence

(0_. R) +* ((0,n) --> ((1. R),(1. R))) is sequence of R

end;
let n be Nat;

coherence

(0_. R) +* ((0,n) --> ((1. R),(1. R))) is sequence of R

proof end;

:: deftheorem defines npoly RING_5:def 3 :

for R being non empty unital doubleLoopStr

for n being Nat holds npoly (R,n) = (0_. R) +* ((0,n) --> ((1. R),(1. R)));

for R being non empty unital doubleLoopStr

for n being Nat holds npoly (R,n) = (0_. R) +* ((0,n) --> ((1. R),(1. R)));

registration

let R be non empty unital doubleLoopStr ;

let n be Nat;

coherence

npoly (R,n) is finite-Support

end;
let n be Nat;

coherence

npoly (R,n) is finite-Support

proof end;

lem6: for n being Nat

for R being non degenerated unital doubleLoopStr holds deg (npoly (R,n)) = n

proof end;

registration

let R be non degenerated unital doubleLoopStr ;

let n be Nat;

coherence

not npoly (R,n) is zero

end;
let n be Nat;

coherence

not npoly (R,n) is zero

proof end;

theorem :: RING_5:43

for n being Nat

for R being non degenerated unital doubleLoopStr holds deg (npoly (R,n)) = n by lem6;

for R being non degenerated unital doubleLoopStr holds deg (npoly (R,n)) = n by lem6;

theorem lem1a: :: RING_5:46

for R being non degenerated Ring

for n being non zero Nat

for x being Element of R holds eval ((npoly (R,n)),x) = (x |^ n) + (1. R)

for n being non zero Nat

for x being Element of R holds eval ((npoly (R,n)),x) = (x |^ n) + (1. R)

proof end;

registration
end;

definition

let R be Ring;

ex b_{1} being Polynomial of R ex F being non empty FinSequence of (Polynom-Ring R) st

( b_{1} = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) )

end;
mode Ppoly of R -> Polynomial of R means :dpp1: :: RING_5:def 4

ex F being non empty FinSequence of (Polynom-Ring R) st

( it = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) );

existence ex F being non empty FinSequence of (Polynom-Ring R) st

( it = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) );

ex b

( b

ex a being Element of R st F . i = rpoly (1,a) ) )

proof end;

:: deftheorem dpp1 defines Ppoly RING_5:def 4 :

for R being Ring

for b_{2} being Polynomial of R holds

( b_{2} is Ppoly of R iff ex F being non empty FinSequence of (Polynom-Ring R) st

( b_{2} = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) ) );

for R being Ring

for b

( b

( b

ex a being Element of R st F . i = rpoly (1,a) ) ) );

lemppoly: for R being domRing

for F being non empty FinSequence of (Polynom-Ring R)

for p being Polynomial of R st p = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) holds

deg p = len F

proof end;

cc2: for R being domRing

for p being Ppoly of R holds LC p = 1. R

proof end;

registration

let R be domRing;

coherence

for b_{1} being Ppoly of R holds

( not b_{1} is constant & b_{1} is monic & b_{1} is with_roots )

end;
coherence

for b

( not b

proof end;

lempolybag1: for R being domRing

for a being Element of R

for F being non empty FinSequence of (Polynom-Ring R) st ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

proof end;

lempolybag: for R being domRing

for B being bag of the carrier of R st card (support B) = 1 holds

ex p being Ppoly of R st

( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )

proof end;

definition

let R be domRing;

let B be non zero bag of the carrier of R;

ex b_{1} being Ppoly of R st

( deg b_{1} = card B & ( for a being Element of R holds multiplicity (b_{1},a) = B . a ) )

end;
let B be non zero bag of the carrier of R;

mode Ppoly of R,B -> Ppoly of R means :dpp: :: RING_5:def 5

( deg it = card B & ( for a being Element of R holds multiplicity (it,a) = B . a ) );

existence ( deg it = card B & ( for a being Element of R holds multiplicity (it,a) = B . a ) );

ex b

( deg b

proof end;

:: deftheorem dpp defines Ppoly RING_5:def 5 :

for R being domRing

for B being non zero bag of the carrier of R

for b_{3} being Ppoly of R holds

( b_{3} is Ppoly of R,B iff ( deg b_{3} = card B & ( for a being Element of R holds multiplicity (b_{3},a) = B . a ) ) );

for R being domRing

for B being non zero bag of the carrier of R

for b

( b

theorem :: RING_5:53

for R being domRing

for B being non zero bag of the carrier of R

for p being Ppoly of R,B

for a being Element of R st a in support B holds

eval (p,a) = 0. R

for B being non zero bag of the carrier of R

for p being Ppoly of R,B

for a being Element of R st a in support B holds

eval (p,a) = 0. R

proof end;

theorem pf1: :: RING_5:54

for R being domRing

for B being non zero bag of the carrier of R

for p being Ppoly of R,B

for a being Element of R holds

( (rpoly (1,a)) `^ (B . a) divides p & not (rpoly (1,a)) `^ ((B . a) + 1) divides p )

for B being non zero bag of the carrier of R

for p being Ppoly of R,B

for a being Element of R holds

( (rpoly (1,a)) `^ (B . a) divides p & not (rpoly (1,a)) `^ ((B . a) + 1) divides p )

proof end;

theorem pf2: :: RING_5:55

for R being domRing

for B being non zero bag of the carrier of R

for p being Ppoly of R,B holds BRoots p = B

for B being non zero bag of the carrier of R

for p being Ppoly of R,B holds BRoots p = B

proof end;

theorem lemacf5: :: RING_5:56

for R being domRing

for B being non zero bag of the carrier of R

for p being Ppoly of R,B holds deg p = card (BRoots p)

for B being non zero bag of the carrier of R

for p being Ppoly of R,B holds deg p = card (BRoots p)

proof end;

theorem lemacf2: :: RING_5:58

for R being domRing

for B1, B2 being non zero bag of the carrier of R

for p being Ppoly of R,B1

for q being Ppoly of R,B2 holds p *' q is Ppoly of R,B1 + B2

for B1, B2 being non zero bag of the carrier of R

for p being Ppoly of R,B1

for q being Ppoly of R,B2 holds p *' q is Ppoly of R,B1 + B2

proof end;

definition
end;

theorem m00: :: RING_5:60

for R being domRing

for S being non empty finite Subset of R

for p being Ppoly of R,S holds deg p = card S

for S being non empty finite Subset of R

for p being Ppoly of R,S holds deg p = card S

proof end;

theorem m0: :: RING_5:61

for R being domRing

for S being non empty finite Subset of R

for p being Ppoly of R,S

for a being Element of R st a in S holds

( rpoly (1,a) divides p & not (rpoly (1,a)) `^ 2 divides p )

for S being non empty finite Subset of R

for p being Ppoly of R,S

for a being Element of R st a in S holds

( rpoly (1,a) divides p & not (rpoly (1,a)) `^ 2 divides p )

proof end;

theorem m1: :: RING_5:62

for R being domRing

for S being non empty finite Subset of R

for p being Ppoly of R,S

for a being Element of R st a in S holds

eval (p,a) = 0. R

for S being non empty finite Subset of R

for p being Ppoly of R,S

for a being Element of R st a in S holds

eval (p,a) = 0. R

proof end;

theorem :: RING_5:63

for R being domRing

for S being non empty finite Subset of R

for p being Ppoly of R,S holds Roots p = S

for S being non empty finite Subset of R

for p being Ppoly of R,S holds Roots p = S

proof end;

theorem acf: :: RING_5:64

for R being domRing

for p being non zero with_roots Polynomial of R ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st

( p = q *' r & Roots q = Roots p )

for p being non zero with_roots Polynomial of R ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st

( p = q *' r & Roots q = Roots p )

proof end;

theorem :: RING_5:66

for R being domRing

for p being non constant Polynomial of R holds

( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q )

for p being non constant Polynomial of R holds

( card (BRoots p) = deg p iff ex a being Element of R ex q being Ppoly of R st p = a * q )

proof end;

theorem :: RING_5:67

for R being domRing

for p, q being Polynomial of R st ex S being Subset of R st

( card S = (max ((deg p),(deg q))) + 1 & ( for a being Element of R st a in S holds

eval (p,a) = eval (q,a) ) ) holds

p = q

for p, q being Polynomial of R st ex S being Subset of R st

( card S = (max ((deg p),(deg q))) + 1 & ( for a being Element of R st a in S holds

eval (p,a) = eval (q,a) ) ) holds

p = q

proof end;

registration

let F be algebraic-closed Field;

for b_{1} being non constant Polynomial of F holds b_{1} is with_roots

end;
cluster Function-like V18( omega , the carrier of F) finite-Support non constant -> non constant with_roots for Element of K19(K20(omega, the carrier of F));

coherence for b

proof end;

registration
end;

registration

for b_{1} being finite domRing holds not b_{1} is algebraic-closed
end;

cluster non empty non degenerated finite right_complementable V98() V100() V122() V123() V124() well-unital V146() domRing-like -> finite non algebraic-closed for doubleLoopStr ;

coherence for b

proof end;

registration

for b_{1} being Ring st b_{1} is algebraic-closed holds

b_{1} is almost_right_invertible
end;

cluster non empty right_complementable V98() V122() V123() V124() well-unital V146() algebraic-closed -> almost_right_invertible for doubleLoopStr ;

coherence for b

b

proof end;

theorem cc4: :: RING_5:68

for F being algebraic-closed Field

for p being non constant Polynomial of F ex a being Element of F ex q being Ppoly of F, BRoots p st a * q = p

for p being non constant Polynomial of F ex a being Element of F ex q being Ppoly of F, BRoots p st a * q = p

proof end;

theorem cc3: :: RING_5:69

for F being algebraic-closed Field

for p being non constant monic Polynomial of F holds p is Ppoly of F, BRoots p

for p being non constant monic Polynomial of F holds p is Ppoly of F, BRoots p

proof end;

theorem :: RING_5:70

for F being Field holds

( F is algebraic-closed iff for p being non constant monic Polynomial of F holds p is Ppoly of F )

( F is algebraic-closed iff for p being non constant monic Polynomial of F holds p is Ppoly of F )

proof end;