:: Little {B}ezout Theorem (Factor Theorem)
:: by Piotr Rudnicki
::
:: Copyright (c) 2003-2021 Association of Mizar Users

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem Th1: :: UPROOTS:1
for f being FinSequence of NAT st ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) holds
( Sum f = len f iff f = (len f) |-> 1 )
proof end;

:: Stolen from POLYNOM2
scheme :: UPROOTS:sch 1
IndFinSeq0{ F1() -> Nat, P1[ set ] } :
for i being Element of NAT st 1 <= i & i <= F1() holds
P1[i]
provided
A1: P1 and
A2: for i being Element of NAT st 1 <= i & i < F1() & P1[i] holds
P1[i + 1]
proof end;

theorem Th2: :: UPROOTS:2
for r being FinSequence of L st len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L ) holds
Sum r = (r /. 1) + (r /. 2)
proof end;

definition
let X be set ;
let S be finite Subset of X;
let n be Element of NAT ;
func (S,n) -bag -> Element of Bags X equals :: UPROOTS:def 2
() +* (S --> n);
correctness
coherence
() +* (S --> n) is Element of Bags X
;
proof end;
end;

:: deftheorem UPROOTS:def 1 :
canceled;

:: deftheorem defines -bag UPROOTS:def 2 :
for X being set
for S being finite Subset of X
for n being Element of NAT holds (S,n) -bag = () +* (S --> n);

theorem :: UPROOTS:3
canceled;

theorem :: UPROOTS:4
canceled;

theorem :: UPROOTS:5
canceled;

::$CT 3 theorem Th3: :: UPROOTS:6 for X being set for S being finite Subset of X for n being Element of NAT for i being object st not i in S holds ((S,n) -bag) . i = 0 proof end; theorem Th4: :: UPROOTS:7 for X being set for S being finite Subset of X for n being Element of NAT for i being set st i in S holds ((S,n) -bag) . i = n proof end; theorem Th5: :: UPROOTS:8 for X being set for S being finite Subset of X for n being Element of NAT st n <> 0 holds support ((S,n) -bag) = S proof end; theorem :: UPROOTS:9 for X being set for S being finite Subset of X for n being Element of NAT st ( S is empty or n = 0 ) holds (S,n) -bag = EmptyBag X proof end; theorem Th7: :: UPROOTS:10 for X being set for S, T being finite Subset of X for n being Element of NAT st S misses T holds ((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag) proof end; definition end; definition let A be set ; let b be Rbag of A; func Sum b -> Real means :Def2: :: UPROOTS:def 3 ex f being FinSequence of REAL st ( it = Sum f & f = b * (canFS ()) ); existence ex b1 being Real ex f being FinSequence of REAL st ( b1 = Sum f & f = b * (canFS ()) ) proof end; uniqueness for b1, b2 being Real st ex f being FinSequence of REAL st ( b1 = Sum f & f = b * (canFS ()) ) & ex f being FinSequence of REAL st ( b2 = Sum f & f = b * (canFS ()) ) holds b1 = b2 ; end; :: deftheorem Def2 defines Sum UPROOTS:def 3 : for A being set for b being Rbag of A for b3 being Real holds ( b3 = Sum b iff ex f being FinSequence of REAL st ( b3 = Sum f & f = b * (canFS ()) ) ); notation let A be set ; let b be bag of A; synonym degree b for Sum b; end; definition let A be set ; let b be bag of A; :: original: Sum redefine func degree b -> Element of NAT means :Def3: :: UPROOTS:def 4 ex f being FinSequence of NAT st ( it = Sum f & f = b * (canFS ()) ); coherence Sum b is Element of NAT proof end; compatibility for b1 being Element of NAT holds ( b1 = Sum b iff ex f being FinSequence of NAT st ( b1 = Sum f & f = b * (canFS ()) ) ) proof end; end; :: deftheorem Def3 defines degree UPROOTS:def 4 : for A being set for b being bag of A for b3 being Element of NAT holds ( b3 = degree b iff ex f being FinSequence of NAT st ( b3 = Sum f & f = b * (canFS ()) ) ); theorem Th8: :: UPROOTS:11 for A being set for b being Rbag of A st b = EmptyBag A holds Sum b = 0 proof end; theorem Th9: :: UPROOTS:12 for A being set for b being bag of A st Sum b = 0 holds b = EmptyBag A proof end; theorem Th10: :: UPROOTS:13 for A being set for S being finite Subset of A for b being bag of A holds ( ( S = support b & degree b = card S ) iff b = (S,1) -bag ) proof end; theorem Th11: :: UPROOTS:14 for A being set for S being finite Subset of A for b being Rbag of A st support b c= S holds ex f being FinSequence of REAL st ( f = b * () & Sum b = Sum f ) proof end; theorem Th12: :: UPROOTS:15 for A being set for b, b1, b2 being Rbag of A st b = b1 + b2 holds Sum b = (Sum b1) + (Sum b2) proof end; theorem Th13: :: UPROOTS:16 for L being non empty unital associative commutative multMagma for f, g being FinSequence of L for p being Permutation of (dom f) st g = f * p holds Product g = Product f proof end; definition let L be non empty ZeroStr ; let p be Polynomial of L; attr p is non-zero means :Def4: :: UPROOTS:def 5 p <> 0_. L; end; :: deftheorem Def4 defines non-zero UPROOTS:def 5 : for L being non empty ZeroStr for p being Polynomial of L holds ( p is non-zero iff p <> 0_. L ); theorem Th14: :: UPROOTS:17 for L being non empty ZeroStr for p being Polynomial of L holds ( p is non-zero iff len p > 0 ) proof end; registration let L be non trivial ZeroStr ; existence ex b1 being Polynomial of L st b1 is non-zero proof end; end; registration let L be non empty non degenerated multLoopStr_0 ; let x be Element of L; cluster <%x,(1. L)%> -> non-zero ; correctness coherence <%x,(1. L)%> is non-zero ; proof end; end; theorem Th15: :: UPROOTS:18 for L being non empty ZeroStr for p being Polynomial of L st len p > 0 holds p . ((len p) -' 1) <> 0. L proof end; theorem Th16: :: UPROOTS:19 for L being non empty ZeroStr for p being AlgSequence of L st len p = 1 holds ( p = <%(p . 0)%> & p . 0 <> 0. L ) proof end; theorem Th17: :: UPROOTS:20 for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L holds p *' (0_. L) = 0_. L proof end; registration existence ex b1 being non empty unital doubleLoopStr st ( b1 is algebraic-closed & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is distributive & b1 is domRing-like & not b1 is degenerated ) proof end; end; theorem Th18: :: UPROOTS:21 for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being Polynomial of L holds ( not p *' q = 0_. L or p = 0_. L or q = 0_. L ) proof end; registration end; registration let L be domRing; let p, q be non-zero Polynomial of L; cluster p *' q -> non-zero ; correctness coherence p *' q is non-zero ; by Th18; end; theorem :: UPROOTS:22 for L being non degenerated comRing for p, q being Polynomial of L holds () \/ () c= Roots (p *' q) proof end; theorem Th20: :: UPROOTS:23 for L being domRing for p, q being Polynomial of L holds Roots (p *' q) = () \/ () proof end; theorem Th21: :: UPROOTS:24 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p being Polynomial of L for pc being Element of () st p = pc holds - p = - pc proof end; theorem Th22: :: UPROOTS:25 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L for pc, qc being Element of () st p = pc & q = qc holds p - q = pc - qc proof end; theorem Th23: :: UPROOTS:26 for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r) proof end; theorem Th24: :: UPROOTS:27 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L st p - q = 0_. L holds p = q proof end; theorem Th25: :: UPROOTS:28 for L being non empty right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds q = r proof end; theorem Th26: :: UPROOTS:29 for L being domRing for n being Element of NAT for p being Polynomial of L st p <> 0_. L holds p ^ n <> 0_. L proof end; theorem Th27: :: UPROOTS:30 for L being comRing for i, j being Nat for p being Polynomial of L holds (p ^ i) *' (p ^ j) = p ^ (i + j) proof end; theorem Th28: :: UPROOTS:31 for L being non empty multLoopStr_0 holds 1_. L = <%(1. L)%> proof end; theorem :: UPROOTS:32 for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr for p being Polynomial of L holds p *' <%(1. L)%> = p proof end; theorem Th30: :: UPROOTS:33 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds len (p *' q) = 0 proof end; theorem Th31: :: UPROOTS:34 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for p, q being Polynomial of L st p *' q is non-zero holds ( p is non-zero & q is non-zero ) proof end; theorem :: UPROOTS:35 for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds 0 < len (p *' q) proof end; theorem Th33: :: UPROOTS:36 for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative domRing-like doubleLoopStr for p, q being Polynomial of L st 1 < len p & 1 < len q holds len p < len (p *' q) proof end; theorem Th34: :: UPROOTS:37 for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr for a, b being Element of L for p being Polynomial of L holds ( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) ) proof end; theorem Th35: :: UPROOTS:38 for L being non empty non degenerated right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr for r being Element of L for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1 proof end; theorem Th36: :: UPROOTS:39 for L being non degenerated comRing for x being Element of L for i being Nat holds len (<%x,(1. L)%> ^ i) = i + 1 proof end; registration let L be non degenerated comRing; let x be Element of L; let n be Nat; cluster <%x,(1. L)%> ^ n -> non-zero ; correctness coherence <%x,(1. L)%> ^ n is non-zero ; proof end; end; theorem Th37: :: UPROOTS:40 for L being non degenerated comRing for x being Element of L for q being non-zero Polynomial of L for i being Nat holds len ((<%x,(1. L)%> ^ i) *' q) = i + (len q) proof end; theorem Th38: :: UPROOTS:41 for L being non empty non degenerated right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr for r being Element of L for p, q being Polynomial of L st p = <%r,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds q . ((len q) -' 1) = 1. L proof end; definition let L be non empty ZeroStr ; let p be Polynomial of L; let n be Nat; func poly_shift (p,n) -> Polynomial of L means :Def5: :: UPROOTS:def 6 for i being Nat holds it . i = p . (n + i); existence ex b1 being Polynomial of L st for i being Nat holds b1 . i = p . (n + i) proof end; uniqueness for b1, b2 being Polynomial of L st ( for i being Nat holds b1 . i = p . (n + i) ) & ( for i being Nat holds b2 . i = p . (n + i) ) holds b1 = b2 proof end; end; :: deftheorem Def5 defines poly_shift UPROOTS:def 6 : for L being non empty ZeroStr for p being Polynomial of L for n being Nat for b4 being Polynomial of L holds ( b4 = poly_shift (p,n) iff for i being Nat holds b4 . i = p . (n + i) ); theorem Th39: :: UPROOTS:42 for L being non empty ZeroStr for p being Polynomial of L holds poly_shift (p,0) = p proof end; theorem Th40: :: UPROOTS:43 for L being non empty ZeroStr for n being Element of NAT for p being Polynomial of L st n >= len p holds poly_shift (p,n) = 0_. L proof end; theorem Th41: :: UPROOTS:44 for L being non empty non degenerated multLoopStr_0 for n being Element of NAT for p being Polynomial of L st n <= len p holds (len (poly_shift (p,n))) + n = len p proof end; theorem Th42: :: UPROOTS:45 for L being non degenerated comRing for x being Element of L for n being Element of NAT for p being Polynomial of L st n < len p holds eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n) proof end; theorem Th43: :: UPROOTS:46 for L being non degenerated comRing for p being Polynomial of L st len p = 1 holds Roots p = {} proof end; definition let L be non degenerated comRing; let r be Element of L; let p be Polynomial of L; assume A1: r is_a_root_of p ; func poly_quotient (p,r) -> Polynomial of L means :Def6: :: UPROOTS:def 7 ( (len it) + 1 = len p & ( for i being Nat holds it . i = eval ((poly_shift (p,(i + 1))),r) ) ) if len p > 0 otherwise it = 0_. L; existence ( ( len p > 0 implies ex b1 being Polynomial of L st ( (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) & ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) ) proof end; uniqueness for b1, b2 being Polynomial of L holds ( ( len p > 0 & (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len b2) + 1 = len p & ( for i being Nat holds b2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies b1 = b2 ) & ( not len p > 0 & b1 = 0_. L & b2 = 0_. L implies b1 = b2 ) ) proof end; consistency for b1 being Polynomial of L holds verum ; end; :: deftheorem Def6 defines poly_quotient UPROOTS:def 7 : for L being non degenerated comRing for r being Element of L for p being Polynomial of L st r is_a_root_of p holds for b4 being Polynomial of L holds ( ( len p > 0 implies ( b4 = poly_quotient (p,r) iff ( (len b4) + 1 = len p & ( for i being Nat holds b4 . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) ) & ( not len p > 0 implies ( b4 = poly_quotient (p,r) iff b4 = 0_. L ) ) ); theorem Th44: :: UPROOTS:47 for L being non degenerated comRing for r being Element of L for p being non-zero Polynomial of L st r is_a_root_of p holds len (poly_quotient (p,r)) > 0 proof end; theorem Th45: :: UPROOTS:48 for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr for x being Element of L holds Roots <%(- x),(1. L)%> = {x} proof end; theorem Th46: :: UPROOTS:49 for L being non trivial comRing for x being Element of L for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds x is_a_root_of p proof end; :: Little Bezout Theorem (Factor Theorem) theorem Th47: :: UPROOTS:50 for L being non degenerated comRing for r being Element of L for p being Polynomial of L st r is_a_root_of p holds p = <%(- r),(1. L)%> *' (poly_quotient (p,r)) proof end; theorem :: UPROOTS:51 for L being non degenerated comRing for r being Element of L for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds r is_a_root_of p proof end; Lm1: now :: thesis: for L being domRing for p being non-zero Polynomial of L holds ( Roots p is finite & ex n being Element of NAT st ( n = card () & n < len p ) ) let L be domRing; :: thesis: for p being non-zero Polynomial of L holds ( Roots p is finite & ex n being Element of NAT st ( n = card () & n < len p ) ) let p be non-zero Polynomial of L; :: thesis: ( Roots p is finite & ex n being Element of NAT st ( n = card () & n < len p ) ) defpred S1[ Nat] means for p being Polynomial of L st len p =$1 holds
( Roots p is finite & ex n being Element of NAT st
( n = card () & n < len p ) );
p <> 0_. L by Def4;
then len p <> 0 by POLYNOM4:5;
then A1: len p >= 0 + 1 by NAT_1:13;
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1 and
A3: S1[n] ; :: thesis: S1[n + 1]
let p be Polynomial of L; :: thesis: ( len p = n + 1 implies ( Roots p is finite & ex n being Element of NAT st
( n = card () & n < len p ) ) )

assume A4: len p = n + 1 ; :: thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card () & n < len p ) )

per cases ( p is with_roots or not p is with_roots ) ;
suppose p is with_roots ; :: thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card () & n < len p ) )

then consider x being Element of L such that
A5: x is_a_root_of p ;
set r = <%(- x),(1. L)%>;
set pq = poly_quotient (p,x);
A6: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by ;
then A7: Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient (p,x))) by Th20;
A8: Roots <%(- x),(1. L)%> = {x} by Th45;
then reconsider Rr = Roots <%(- x),(1. L)%> as finite set ;
A9: (len (poly_quotient (p,x))) + 1 = len p by A4, A5, Def6;
then consider k being Element of NAT such that
A10: k = card (Roots (poly_quotient (p,x))) and
A11: k < len (poly_quotient (p,x)) by A3, A4;
reconsider Rpq = Roots (poly_quotient (p,x)) as finite set by A3, A4, A9;
reconsider Rp = Rpq \/ Rr as finite set ;
card Rr = 1 by ;
then A12: card Rp <= k + 1 by ;
Roots (poly_quotient (p,x)) is finite by A3, A4, A9;
hence Roots p is finite by A8, A7; :: thesis: ex n being Element of NAT st
( n = card () & n < len p )

take m = card Rp; :: thesis: ( m = card () & m < len p )
thus m = card () by ; :: thesis: m < len p
k + 1 < n + 1 by ;
hence m < len p by ; :: thesis: verum
end;
suppose A13: not p is with_roots ; :: thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card () & n < len p ) )

A14: now :: thesis: not Roots p <> {}
assume Roots p <> {} ; :: thesis: contradiction
then consider x being object such that
A15: x in Roots p by XBOOLE_0:def 1;
reconsider x = x as Element of L by A15;
x is_a_root_of p by ;
hence contradiction by A13; :: thesis: verum
end;
hence Roots p is finite ; :: thesis: ex n being Element of NAT st
( n = card () & n < len p )

take 0 ; :: thesis: ( 0 = card () & 0 < len p )
thus 0 = card () by A14; :: thesis:
thus 0 < len p by A4; :: thesis: verum
end;
end;
end;
A16: S1
proof
let p be Polynomial of L; :: thesis: ( len p = 1 implies ( Roots p is finite & ex n being Element of NAT st
( n = card () & n < len p ) ) )

assume A17: len p = 1 ; :: thesis: ( Roots p is finite & ex n being Element of NAT st
( n = card () & n < len p ) )

hence Roots p is finite by Th43; :: thesis: ex n being Element of NAT st
( n = card () & n < len p )

take 0 ; :: thesis: ( 0 = card () & 0 < len p )
thus 0 = card () by ; :: thesis:
thus 0 < len p by A17; :: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch 8(A16, A2);
hence ( Roots p is finite & ex n being Element of NAT st
( n = card () & n < len p ) ) by A1; :: thesis: verum
end;

registration
let L be domRing;
let p be non-zero Polynomial of L;
correctness
coherence
Roots p is finite
;
by Lm1;
end;

definition
let L be non degenerated comRing;
let x be Element of L;
let p be non-zero Polynomial of L;
func multiplicity (p,x) -> Element of NAT means :Def7: :: UPROOTS:def 8
ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> ^ k) *' q } & it = max F );
existence
ex b1 being Element of NAT ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> ^ k) *' q } & b1 = max F )
proof end;
uniqueness
for b1, b2 being Element of NAT st ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> ^ k) *' q } & b1 = max F ) & ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> ^ k) *' q } & b2 = max F ) holds
b1 = b2
;
end;

:: deftheorem Def7 defines multiplicity UPROOTS:def 8 :
for L being non degenerated comRing
for x being Element of L
for p being non-zero Polynomial of L
for b4 being Element of NAT holds
( b4 = multiplicity (p,x) iff ex F being non empty finite Subset of NAT st
( F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> ^ k) *' q } & b4 = max F ) );

theorem Th49: :: UPROOTS:52
for L being non degenerated comRing
for p being non-zero Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff multiplicity (p,x) >= 1 )
proof end;

theorem Th50: :: UPROOTS:53
for L being non degenerated comRing
for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1
proof end;

definition
let L be domRing;
let p be non-zero Polynomial of L;
func BRoots p -> bag of the carrier of L means :Def8: :: UPROOTS:def 9
( support it = Roots p & ( for x being Element of L holds it . x = multiplicity (p,x) ) );
existence
ex b1 being bag of the carrier of L st
( support b1 = Roots p & ( for x being Element of L holds b1 . x = multiplicity (p,x) ) )
proof end;
uniqueness
for b1, b2 being bag of the carrier of L st support b1 = Roots p & ( for x being Element of L holds b1 . x = multiplicity (p,x) ) & support b2 = Roots p & ( for x being Element of L holds b2 . x = multiplicity (p,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines BRoots UPROOTS:def 9 :
for L being domRing
for p being non-zero Polynomial of L
for b3 being bag of the carrier of L holds
( b3 = BRoots p iff ( support b3 = Roots p & ( for x being Element of L holds b3 . x = multiplicity (p,x) ) ) );

theorem Th51: :: UPROOTS:54
for L being domRing
for x being Element of L holds BRoots <%(- x),(1. L)%> = ({x},1) -bag
proof end;

theorem Th52: :: UPROOTS:55
for L being domRing
for x being Element of L
for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
proof end;

theorem Th53: :: UPROOTS:56
for L being domRing
for p, q being non-zero Polynomial of L holds BRoots (p *' q) = () + ()
proof end;

Lm2: now :: thesis: for L being domRing
for p, q being non-zero Polynomial of L holds degree (BRoots (p *' q)) = (degree ()) + (degree ())
let L be domRing; :: thesis: for p, q being non-zero Polynomial of L holds degree (BRoots (p *' q)) = (degree ()) + (degree ())
let p, q be non-zero Polynomial of L; :: thesis: degree (BRoots (p *' q)) = (degree ()) + (degree ())
BRoots (p *' q) = () + () by Th53;
hence degree (BRoots (p *' q)) = (degree ()) + (degree ()) by Th12; :: thesis: verum
end;

theorem Th54: :: UPROOTS:57
for L being domRing
for p being non-zero Polynomial of L st len p = 1 holds
degree () = 0
proof end;

theorem Th55: :: UPROOTS:58
for L being domRing
for x being Element of L
for n being Nat holds degree (BRoots (<%(- x),(1. L)%> ^ n)) = n
proof end;

theorem :: UPROOTS:59
for L being algebraic-closed domRing
for p being non-zero Polynomial of L holds degree () = (len p) -' 1
proof end;

definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let c be Element of L;
let n be Element of NAT ;
func fpoly_mult_root (c,n) -> FinSequence of () means :Def9: :: UPROOTS:def 10
( len it = n & ( for i being Element of NAT st i in dom it holds
it . i = <%(- c),(1. L)%> ) );
existence
ex b1 being FinSequence of () st
( len b1 = n & ( for i being Element of NAT st i in dom b1 holds
b1 . i = <%(- c),(1. L)%> ) )
proof end;
uniqueness
for b1, b2 being FinSequence of () st len b1 = n & ( for i being Element of NAT st i in dom b1 holds
b1 . i = <%(- c),(1. L)%> ) & len b2 = n & ( for i being Element of NAT st i in dom b2 holds
b2 . i = <%(- c),(1. L)%> ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines fpoly_mult_root UPROOTS:def 10 :
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for c being Element of L
for n being Element of NAT
for b4 being FinSequence of () holds
( b4 = fpoly_mult_root (c,n) iff ( len b4 = n & ( for i being Element of NAT st i in dom b4 holds
b4 . i = <%(- c),(1. L)%> ) ) );

definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let b be bag of the carrier of L;
func poly_with_roots b -> Polynomial of L means :Def10: :: UPROOTS:def 11
ex f being FinSequence of the carrier of () * ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it = Product () );
existence
ex b1 being Polynomial of L ex f being FinSequence of the carrier of () * ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b1 = Product () )
proof end;
uniqueness
for b1, b2 being Polynomial of L st ex f being FinSequence of the carrier of () * ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b1 = Product () ) & ex f being FinSequence of the carrier of () * ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b2 = Product () ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines poly_with_roots UPROOTS:def 11 :
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for b3 being Polynomial of L holds
( b3 = poly_with_roots b iff ex f being FinSequence of the carrier of () * ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & b3 = Product () ) );

theorem Th57: :: UPROOTS:60
for L being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr holds poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%>
proof end;

theorem Th58: :: UPROOTS:61
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%>
proof end;

theorem Th59: :: UPROOTS:62
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for f being FinSequence of the carrier of () *
for s being FinSequence of L st len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len () = degree b
proof end;

theorem Th60: :: UPROOTS:63
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for f being FinSequence of the carrier of () *
for s being FinSequence of L
for c being Element of L st len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card (() " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card (() " {<%(- c),(1. L)%>}) = 0 ) )
proof end;

theorem Th61: :: UPROOTS:64
for L being comRing
for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = () *' ()
proof end;

theorem :: UPROOTS:65
for L being algebraic-closed domRing
for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds
p = poly_with_roots ()
proof end;

theorem :: UPROOTS:66
for L being comRing
for s being non empty finite Subset of L
for f being FinSequence of () st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = () . i holds
f . i = <%(- c),(1. L)%> ) holds
poly_with_roots ((s,1) -bag) = Product f
proof end;

theorem :: UPROOTS:67
for L being non trivial comRing
for s being non empty finite Subset of L
for x being Element of L
for f being FinSequence of L st len f = card s & ( for i being Element of NAT
for c being Element of L st i in dom f & c = () . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f
proof end;