:: On Roots of Polynomials and Algebraically Closed Fields
:: by Christoph Schwarzweller
::
:: Received August 30, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


registration
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 b1 being Nat st
( not b1 is trivial & not b1 is prime )
by NAT_2:def 1, INT_2:29;
end;

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;

theorem XX: :: RING_5:1
for n being even Nat
for x being Element of F_Real holds x |^ n >= 0. F_Real
proof end;

theorem prl3: :: RING_5:2
for R being Ring
for a being Element of R holds 2 '*' a = a + a
proof end;

theorem :: RING_5:3
for R being Ring
for a being Element of R holds a |^ 2 = a * a by prl4;

registration
let F be Field;
let a be Element of F;
reduce a / (1. F) to a;
reducibility
a / (1. F) = a
proof end;
end;

registration
cluster Z/ 2 -> non trivial almost_left_invertible ;
coherence
( not Z/ 2 is trivial & Z/ 2 is almost_left_invertible )
by INT_2:28;
end;

registration
let n be non trivial non prime Nat;
cluster Z/ n -> non domRing-like ;
coherence
not Z/ n is domRing-like
proof end;
end;

registration
cluster Z/ 6 -> non degenerated ;
coherence
not Z/ 6 is degenerated
proof end;
end;

registration
let R be non degenerated Ring;
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 b1 being non zero Polynomial of R holds b1 is non-zero
;
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 b1 being Polynomial of R st b1 is monic holds
not b1 is zero
;
end;

registration
let R be non degenerated Ring;
let p be non zero Polynomial of R;
cluster degree p -> natural ;
coherence
deg p is natural
;
end;

registration
let R be Ring;
let p be zero Polynomial of R;
let q be Polynomial of R;
cluster p *' q -> zero ;
coherence
p *' q is zero
proof end;
cluster q *' p -> zero ;
coherence
q *' p is zero
proof end;
end;

registration
let R be Ring;
let p be zero Polynomial of R;
let q be Polynomial of R;
reduce p + q to q;
reducibility
p + q = q
proof end;
reduce q + p to q;
reducibility
q + p = q
;
end;

registration
let R be Ring;
let p be Polynomial of R;
reduce p *' (0_. R) to 0_. R;
reducibility
p *' (0_. R) = 0_. R
by POLYNOM3:34;
reduce p *' (1_. R) to p;
reducibility
p *' (1_. R) = p
by POLYNOM3:35;
reduce (0_. R) *' p to 0_. R;
reducibility
(0_. R) *' p = 0_. R
by POLYNOM4:2;
reduce (1_. R) *' p to p;
reducibility
(1_. R) *' p = p
by RING_4:12;
end;

registration
let R be Ring;
let p be Polynomial of R;
reduce (1. R) * p to p;
reducibility
(1. R) * p = p
by POLYNOM5:27;
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
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)
proof end;

theorem :: RING_5:6
for R being domRing
for a being Element of R holds LC (a | R) = a
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))
proof end;

theorem evconst: :: RING_5:8
for R being Ring
for a, b being Element of R holds eval ((a | R),b) = a
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
let R be domRing;
let p, q be monic Polynomial of R;
cluster p *' q -> monic ;
coherence
p *' q is monic
proof end;
end;

registration
let R be domRing;
let a be Element of R;
let k be Nat;
cluster (rpoly (1,a)) `^ k -> non zero monic ;
coherence
( not (rpoly (1,a)) `^ k is zero & (rpoly (1,a)) `^ k is monic )
proof end;
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
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)
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 )
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 )
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
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
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 )
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 )
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 )
proof end;

registration
let R be domRing;
let p be non zero Polynomial of R;
let b be non zero Element of R;
cluster b * p -> non zero ;
coherence
not b * p is zero
proof end;
end;

registration
let R be non degenerated Ring;
cluster 1_. R -> non with_roots ;
coherence
not 1_. R is with_roots
proof end;
end;

registration
let R be non degenerated Ring;
let a be non zero Element of R;
cluster a | R -> non with_roots ;
coherence
not a | R is with_roots
proof end;
end;

registration
let R be non degenerated Ring;
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 b1 being Polynomial of R st not b1 is zero & b1 is with_roots holds
not b1 is constant
proof end;
end;

registration
let R be non degenerated Ring;
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 b1 being Polynomial of R st not b1 is with_roots holds
not b1 is zero
;
end;

registration
let R be non degenerated Ring;
let a be Element of R;
cluster rpoly (1,a) -> non zero with_roots ;
coherence
( not rpoly (1,a) is zero & rpoly (1,a) is with_roots )
by HURWITZ:30, POLYNOM5:def 8;
end;

registration
let R be non degenerated Ring;
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 b1 being Polynomial of R st
( not b1 is zero & not b1 is with_roots )
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 b1 being Polynomial of R st
( not b1 is zero & b1 is with_roots )
proof end;
end;

registration
let R be domRing;
let p be non with_roots Polynomial of R;
let a be non zero Element of R;
cluster a * p -> non with_roots ;
coherence
not a * p is with_roots
proof end;
end;

registration
let R be domRing;
let p be with_roots Polynomial of R;
let a be Element of R;
cluster a * p -> with_roots ;
coherence
a * p is with_roots
proof end;
end;

registration
let R be non degenerated comRing;
let p be with_roots Polynomial of R;
let q be Polynomial of R;
cluster p *' q -> with_roots ;
coherence
p *' q is with_roots
proof end;
end;

registration
let R be domRing;
let p, q be non with_roots Polynomial of R;
cluster p *' q -> non with_roots ;
coherence
not p *' q is with_roots
proof end;
end;

registration
let R be non degenerated comRing;
let a be Element of R;
let k be non zero Element of NAT ;
cluster rpoly (k,a) -> non constant monic with_roots ;
coherence
( not rpoly (k,a) is constant & rpoly (k,a) is monic & rpoly (k,a) is with_roots )
proof end;
end;

registration
let R be non degenerated Ring;
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 b1 being Polynomial of R st
( not b1 is constant & b1 is monic )
proof end;
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 ;
cluster (rpoly (n,a)) `^ k -> non constant monic with_roots ;
coherence
( not (rpoly (n,a)) `^ k is constant & (rpoly (n,a)) `^ k is monic & (rpoly (n,a)) `^ k is with_roots )
proof end;
end;

registration
let R be Ring;
let p be with_roots Polynomial of R;
cluster Roots p -> non empty ;
coherence
not Roots p is empty
proof end;
end;

registration
let R be non degenerated Ring;
let p be non with_roots Polynomial of R;
cluster Roots p -> empty ;
coherence
Roots p is empty
proof end;
end;

registration
let R be domRing;
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 b1 being Polynomial of R st
( b1 is monic & b1 is with_roots )
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 b1 being Polynomial of R st
( b1 is monic & not b1 is with_roots )
proof end;
end;

theorem ro4: :: RING_5:18
for R being non degenerated Ring
for a being Element of R holds Roots (rpoly (1,a)) = {a}
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
proof end;

theorem :: RING_5:20
not for p, q being Polynomial of (Z/ 6) holds Roots (p *' q) c= (Roots p) \/ (Roots q)
proof end;

theorem div100: :: RING_5:21
for R being domRing
for a, b being Element of R holds
( rpoly (1,a) divides rpoly (1,b) iff a = b )
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;

theorem degpoly: :: RING_5:22
for R being domRing
for p being non zero Polynomial of R holds card (Roots p) <= deg p
proof end;

notation
let X be non empty set ;
let B be bag of X;
synonym card B for Sum B;
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 ;
cluster Relation-like X -defined RAT -valued Function-like non empty total V109() V110() V111() V112() finite-support zero for set ;
existence
ex b1 being bag of X st b1 is zero
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 b1 being bag of X holds b1 is zero
proof end;
end;

registration
let X be non empty set ;
let b1, b2 be bag of X;
cluster K218(b1,b2) -> X -defined ;
coherence
b1 + b2 is X -defined
;
end;

registration
let X be non empty set ;
let b1, b2 be bag of X;
cluster K218(b1,b2) -> total ;
coherence
b1 + b2 is total
;
end;

theorem bag1a: :: RING_5:23
for X being non empty set
for b being bag of X holds
( card b = 0 iff support b = {} )
proof end;

theorem bbag: :: RING_5:24
for X being non empty set
for b being bag of X holds
( b is zero iff support b = {} )
proof end;

theorem :: RING_5:25
for X being non empty set
for b being bag of X holds
( b is zero iff rng b = {0} ) by bbbag;

registration
let X be non empty set ;
let b1 be non zero bag of X;
let b2 be bag of X;
cluster K218(b1,b2) -> non zero ;
coherence
not b1 + b2 is zero
proof end;
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
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 ) )
proof end;

definition
let X be set ;
let S be finite Subset of X;
func Bag S -> bag of X equals :: RING_5:def 1
(S,1) -bag ;
coherence
(S,1) -bag is bag of X
;
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 ;

registration
let X be non empty set ;
let S be non empty finite Subset of X;
cluster Bag S -> non zero ;
coherence
not Bag S is zero
proof end;
end;

definition
let X be non empty set ;
let b be bag of X;
let a be Element of X;
func b \ a -> bag of X equals :: RING_5:def 2
b +* (a,0);
coherence
b +* (a,0) is bag of X
;
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);

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

registration
let R be domRing;
let p be non zero with_roots Polynomial of R;
cluster BRoots p -> non zero ;
coherence
not BRoots p is zero
proof end;
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 )
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 ) )
proof end;

theorem BR5aa: :: RING_5:34
for R being domRing
for a being Element of R holds multiplicity ((rpoly (1,a)),a) = 1
proof end;

theorem BR5aaa: :: RING_5:35
for R being domRing
for a, b being Element of R st b <> a holds
multiplicity ((rpoly (1,a)),b) = 0
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)
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
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
proof end;

theorem bag1: :: RING_5:39
for R being domRing
for a being non zero Element of R holds card (BRoots (a | R)) = 0
proof end;

theorem bag2: :: RING_5:40
for R being domRing
for a being Element of R holds card (BRoots (rpoly (1,a))) = 1
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))
proof end;

theorem :: RING_5:42
for R being domRing
for p being non zero Polynomial of R holds card (BRoots p) <= deg p
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;
func npoly (R,n) -> sequence of R equals :: RING_5:def 3
(0_. R) +* ((0,n) --> ((1. R),(1. R)));
coherence
(0_. R) +* ((0,n) --> ((1. R),(1. R))) is sequence of R
proof end;
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)));

registration
let R be non empty unital doubleLoopStr ;
let n be Nat;
cluster npoly (R,n) -> finite-Support ;
coherence
npoly (R,n) is finite-Support
proof end;
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;
cluster npoly (R,n) -> non zero ;
coherence
not npoly (R,n) is zero
proof end;
end;

theorem :: RING_5:43
for n being Nat
for R being non degenerated unital doubleLoopStr holds deg (npoly (R,n)) = n by lem6;

theorem :: RING_5:44
for n being Nat
for R being non degenerated unital doubleLoopStr holds LC (npoly (R,n)) = 1. R
proof end;

theorem lem1e: :: RING_5:45
for R being non degenerated Ring
for x being Element of R holds eval ((npoly (R,0)),x) = 1. R
proof end;

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

theorem lem1: :: RING_5:47
for n being even Nat
for x being Element of F_Real holds eval ((npoly (F_Real,n)),x) > 0. F_Real
proof end;

theorem lem1c: :: RING_5:48
for n being odd Nat holds eval ((npoly (F_Real,n)),(- (1. F_Real))) = 0. F_Real
proof end;

theorem lem1b: :: RING_5:49
eval ((npoly ((Z/ 2),2)),(1. (Z/ 2))) = 0. (Z/ 2)
proof end;

registration
let n be even Nat;
cluster npoly (F_Real,n) -> non with_roots ;
coherence
not npoly (F_Real,n) is with_roots
proof end;
end;

registration
let n be odd Nat;
cluster npoly (F_Real,n) -> with_roots ;
coherence
npoly (F_Real,n) is with_roots
proof end;
end;

registration
cluster npoly ((Z/ 2),2) -> with_roots ;
coherence
npoly ((Z/ 2),2) is with_roots
by POLYNOM5:def 7, POLYNOM5:def 8, lem1b;
end;

definition
let R be Ring;
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 b1 being Polynomial of R ex F being non empty FinSequence of (Polynom-Ring R) st
( b1 = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) )
proof end;
end;

:: deftheorem dpp1 defines Ppoly RING_5:def 4 :
for R being Ring
for b2 being Polynomial of R holds
( b2 is Ppoly of R iff ex F being non empty FinSequence of (Polynom-Ring R) st
( b2 = Product F & ( for i being Nat st i in dom F holds
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;
cluster -> non constant monic with_roots for Ppoly of R;
coherence
for b1 being Ppoly of R holds
( not b1 is constant & b1 is monic & b1 is with_roots )
proof end;
end;

theorem :: RING_5:50
for R being domRing
for p being Ppoly of R holds LC p = 1. R by cc2;

theorem lemppoly1: :: RING_5:51
for R being domRing
for a being Element of R holds rpoly (1,a) is Ppoly of R
proof end;

theorem lemppoly3: :: RING_5:52
for R being domRing
for p, q being Ppoly of R holds p *' q is Ppoly of R
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;
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
ex b1 being Ppoly of R st
( deg b1 = card B & ( for a being Element of R holds multiplicity (b1,a) = B . a ) )
proof end;
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 b3 being Ppoly of R holds
( b3 is Ppoly of R,B iff ( deg b3 = card B & ( for a being Element of R holds multiplicity (b3,a) = B . a ) ) );

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

theorem lemacf: :: RING_5:57
for R being domRing
for a being Element of R holds rpoly (1,a) is Ppoly of R, Bag {a}
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
proof end;

theorem lll: :: RING_5:59
for R being domRing
for p being Ppoly of R holds p is Ppoly of R, BRoots p
proof end;

definition
let R be domRing;
let S be non empty finite Subset of R;
mode Ppoly of R,S is Ppoly of R, Bag S;
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
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 )
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
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
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 )
proof end;

theorem :: RING_5:65
for R being domRing
for p being non zero Polynomial of R holds card (Roots p) <= card (BRoots 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 )
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
proof end;

registration
let F be algebraic-closed Field;
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 b1 being non constant Polynomial of F holds b1 is with_roots
proof end;
end;

registration
cluster F_Real -> non algebraic-closed ;
coherence
not F_Real is algebraic-closed
proof end;
end;

registration
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 b1 being finite domRing holds not b1 is algebraic-closed
proof end;
end;

registration
cluster non empty right_complementable V98() V122() V123() V124() well-unital V146() algebraic-closed -> almost_right_invertible for doubleLoopStr ;
coherence
for b1 being Ring st b1 is algebraic-closed holds
b1 is almost_right_invertible
proof end;
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
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
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 )
proof end;