:: 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 b₁ being Nat st
( not b₁ is trivial & not b₁ 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 b₁ being non zero Polynomial of R holds b₁ 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 b₁ being Polynomial of R st b₁ is monic holds
not b₁ 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 b₁ being Polynomial of R st not b₁ is zero & b₁ is with_roots holds
not b₁ 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 b₁ being Polynomial of R st not b₁ is with_roots holds
not b₁ 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 b₁ being Polynomial of R st
( not b₁ is zero & not b₁ 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 b₁ being Polynomial of R st
( not b₁ is zero & b₁ 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 b₁ being Polynomial of R st
( not b₁ is constant & b₁ 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 b₁ being Polynomial of R st
( b₁ is monic & b₁ 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 b₁ being Polynomial of R st
( b₁ is monic & not b₁ 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 b₁ being bag of X st b₁ 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 b₁ being bag of X holds b₁ 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 b₁ being Polynomial of R ex F being non empty FinSequence of (Polynom-Ring R) st
( b₁ = 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 b₂ being Polynomial of R holds
( b₂ is Ppoly of R iff ex F being non empty FinSequence of (Polynom-Ring R) st
( b₂ = 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 b₁ being Ppoly of R holds
( not b₁ is constant & b₁ is monic & b₁ 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 b₁ being Ppoly of R st
( deg b₁ = card B & ( for a being Element of R holds multiplicity (b₁,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 b₃ being Ppoly of R holds
( b₃ is Ppoly of R,B iff ( deg b₃ = card B & ( for a being Element of R holds multiplicity (b₃,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 b₁ being non constant Polynomial of F holds b₁ 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 b₁ being finite domRing holds not b₁ 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 b₁ being Ring st b₁ is algebraic-closed holds
b₁ 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;