:: UPROOTS semantic presentation

theorem Th1: :: UPROOTS:1

for b₁ being natural number holds
( ( b₁ = 1 or b₁ > 1 ) iff not b₁ is empty )

proof end;

theorem Th2: :: UPROOTS:2

for b₁ being FinSequence of NAT st ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ <> 0 ) holds
( Sum b₁ = len b₁ iff b₁ = (len b₁) |-> 1 )

proof end;

scheme :: UPROOTS:sch 1
s1{ F₁() -> FinSequence, P₁[ set , set ] } :

for b₁ being Nat st 1 <= b₁ & b₁ <= len F₁() holds
P₁[b₁,F₁() . b₁]

provided

E3: P₁[1,F₁() . 1] and
E4: for b₁ being Nat st 1 <= b₁ & b₁ < len F₁() & P₁[b₁,F₁() . b₁] holds
P₁[b₁ + 1,F₁() . (b₁ + 1)]

proof end;

theorem Th3: :: UPROOTS:3

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of b₁ st len b₂ >= 2 & ( for b₃ being Nat st 2 < b₃ & b₃ in dom b₂ holds
b₂ . b₃ = 0. b₁ ) holds
Sum b₂ = (b₂ /. 1) + (b₂ /. 2)

proof end;

definition

let c₁ be finite set ;
func canFS c₁ -> FinSequence of a₁ means :Def1: :: UPROOTS:def 1
( len a₂ = card a₁ & ex b₁ being FinSequence st
( len b₁ = card a₁ & ( b₁ . 1 = [(choose a₁),(a₁ \ {(choose a₁)})] or card a₁ = 0 ) & ( for b₂ being Nat st 1 <= b₂ & b₂ < card a₁ holds
for b₃ being set st b₁ . b₂ = b₃ holds
b₁ . (b₂ + 1) = [(choose (b₃ `2 )),((b₃ `2 ) \ {(choose (b₃ `2 ))})] ) & ( for b₂ being Nat st b₂ in dom a₂ holds
a₂ . b₂ = (b₁ . b₂) `1 ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines canFS UPROOTS:def 1 :

theorem Th4: :: UPROOTS:4

for b₁ being finite set holds canFS b₁ is one-to-one

proof end;

theorem Th5: :: UPROOTS:5

for b₁ being finite set holds rng (canFS b₁) = b₁

proof end;

theorem Th6: :: UPROOTS:6

for b₁ being set holds canFS {b₁} = <*b₁*>

proof end;

theorem Th7: :: UPROOTS:7

for b₁ being finite set holds (canFS b₁) " is Function of b₁, Seg (card b₁)

proof end;

definition

let c₁ be set ;
let c₂ be finite Subset of c₁;
let c₃ be Nat;
func c₂,c₃ -bag -> Element of Bags a₁ equals :: UPROOTS:def 2
(EmptyBag a₁) +* (a₂ --> a₃);
correctness

proof end;

end;

:: deftheorem Def2 defines -bag UPROOTS:def 2 :

theorem Th8: :: UPROOTS:8

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Nat
for b₄ being set st not b₄ in b₂ holds
(b₂,b₃ -bag ) . b₄ = 0

proof end;

theorem Th9: :: UPROOTS:9

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Nat
for b₄ being set st b₄ in b₂ holds
(b₂,b₃ -bag ) . b₄ = b₃

proof end;

theorem Th10: :: UPROOTS:10

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Nat st b₃ <> 0 holds
support (b₂,b₃ -bag ) = b₂

proof end;

theorem Th11: :: UPROOTS:11

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Nat st ( b₂ is empty or b₃ = 0 ) holds
b₂,b₃ -bag = EmptyBag b₁

proof end;

theorem Th12: :: UPROOTS:12

for b₁ being set
for b₂, b₃ being finite Subset of b₁
for b₄ being Nat st b₂ misses b₃ holds
(b₂ \/ b₃),b₄ -bag = (b₂,b₄ -bag ) + (b₃,b₄ -bag )

proof end;

definition

let c₁ be set ;
mode Rbag of a₁ is real-yielding finite-support ManySortedSet of a₁;

end;

definition

let c₁ be set ;
let c₂ be Rbag of c₁;
func Sum c₂ -> real number means :Def3: :: UPROOTS:def 3
ex b₁ being FinSequence of REAL st
( a₃ = Sum b₁ & b₁ = a₂ * (canFS (support a₂)) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines Sum UPROOTS:def 3 :

notation

let c₁ be set ;
let c₂ be bag of c₁;
synonym degree c₂ for Sum c₂;

end;

definition

let c₁ be set ;
let c₂ be bag of c₁;
redefine func Sum as degree c₂ -> Nat means :Def4: :: UPROOTS:def 4
ex b₁ being FinSequence of NAT st
( a₃ = Sum b₁ & b₁ = a₂ * (canFS (support a₂)) );
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def4 defines degree UPROOTS:def 4 :

theorem Th13: :: UPROOTS:13

for b₁ being set
for b₂ being Rbag of b₁ st b₂ = EmptyBag b₁ holds
Sum b₂ = 0

proof end;

theorem Th14: :: UPROOTS:14

for b₁ being set
for b₂ being bag of b₁ st Sum b₂ = 0 holds
b₂ = EmptyBag b₁

proof end;

theorem Th15: :: UPROOTS:15

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being bag of b₁ holds
( ( b₂ = support b₃ & degree b₃ = card b₂ ) iff b₃ = b₂,1 -bag )

proof end;

theorem Th16: :: UPROOTS:16

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Rbag of b₁ st support b₃ c= b₂ holds
ex b₄ being FinSequence of REAL st
( b₄ = b₃ * (canFS b₂) & Sum b₃ = Sum b₄ )

proof end;

theorem Th17: :: UPROOTS:17

for b₁ being set
for b₂, b₃, b₄ being Rbag of b₁ st b₂ = b₃ + b₄ holds
Sum b₂ = (Sum b₃) + (Sum b₄)

proof end;

theorem Th18: :: UPROOTS:18

for b₁ being non empty unital associative commutative HGrStr
for b₂, b₃ being FinSequence of b₁
for b₄ being Permutation of dom b₂ st b₃ = b₂ * b₄ holds
Product b₃ = Product b₂

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be Polynomial of c₁;
attr a₂ is non-zero means :Def5: :: UPROOTS:def 5
a₂ <> 0_. a₁;

end;

:: deftheorem Def5 defines non-zero UPROOTS:def 5 :

theorem Th19: :: UPROOTS:19

for b₁ being non empty ZeroStr
for b₂ being Polynomial of b₁ holds
( b₂ is non-zero iff len b₂ > 0 )

proof end;

registration

let c₁ be non empty non trivial ZeroStr ;
cluster non-zero M5( NAT ,the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be non empty non degenerated multLoopStr_0 ;
let c₂ be Element of c₁;
cluster <%a₂,(1. a₁)%> -> non-zero ;
correctness

proof end;

end;

theorem Th20: :: UPROOTS:20

for b₁ being non empty ZeroStr
for b₂ being Polynomial of b₁ st len b₂ > 0 holds
b₂ . ((len b₂) -' 1) <> 0. b₁

proof end;

theorem Th21: :: UPROOTS:21

for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ st len b₂ = 1 holds
( b₂ = <%(b₂ . 0)%> & b₂ . 0 <> 0. b₁ )

proof end;

theorem Th22: :: UPROOTS:22

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂ being Polynomial of b₁ holds b₂ *' (0_. b₁) = 0_. b₁

proof end;

registration

cluster non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non degenerated domRing-like algebraic-closed doubleLoopStr ;
existence

proof end;

end;

theorem Th23: :: UPROOTS:23

for b₁ being non empty add-associative right_zeroed right_complementable distributive domRing-like doubleLoopStr
for b₂, b₃ being Polynomial of b₁ holds
( not b₂ *' b₃ = 0_. b₁ or b₂ = 0_. b₁ or b₃ = 0_. b₁ )

proof end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable distributive domRing-like doubleLoopStr ;
cluster Polynom-Ring a₁ -> domRing-like ;
correctness

proof end;

end;

registration

let c₁ be domRing;
let c₂, c₃ be non-zero Polynomial of c₁;
cluster a₂ *' a₃ -> non-zero ;
correctness

proof end;

end;

theorem Th24: :: UPROOTS:24

for b₁ being non degenerated comRing
for b₂, b₃ being Polynomial of b₁ holds (Roots b₂) \/ (Roots b₃) c= Roots (b₂ *' b₃)

proof end;

theorem Th25: :: UPROOTS:25

for b₁ being domRing
for b₂, b₃ being Polynomial of b₁ holds Roots (b₂ *' b₃) = (Roots b₂) \/ (Roots b₃)

proof end;

theorem Th26: :: UPROOTS:26

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being Polynomial of b₁
for b₃ being Element of (Polynom-Ring b₁) st b₂ = b₃ holds
- b₂ = - b₃

proof end;

theorem Th27: :: UPROOTS:27

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Polynomial of b₁
for b₄, b₅ being Element of (Polynom-Ring b₁) st b₂ = b₄ & b₃ = b₅ holds
b₂ - b₃ = b₄ - b₅

proof end;

theorem Th28: :: UPROOTS:28

for b₁ being non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃, b₄ being Polynomial of b₁ holds (b₂ *' b₃) - (b₂ *' b₄) = b₂ *' (b₃ - b₄)

proof end;

theorem Th29: :: UPROOTS:29

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Polynomial of b₁ st b₂ - b₃ = 0_. b₁ holds
b₂ = b₃

proof end;

theorem Th30: :: UPROOTS:30

for b₁ being non empty Abelian add-associative right_zeroed right_complementable distributive domRing-like doubleLoopStr
for b₂, b₃, b₄ being Polynomial of b₁ st b₂ <> 0_. b₁ & b₂ *' b₃ = b₂ *' b₄ holds
b₃ = b₄

proof end;

theorem Th31: :: UPROOTS:31

for b₁ being domRing
for b₂ being Nat
for b₃ being Polynomial of b₁ st b₃ <> 0_. b₁ holds
b₃ `^ b₂ <> 0_. b₁

proof end;

theorem Th32: :: UPROOTS:32

for b₁ being comRing
for b₂, b₃ being Nat
for b₄ being Polynomial of b₁ holds (b₄ `^ b₂) *' (b₄ `^ b₃) = b₄ `^ (b₂ + b₃)

proof end;

theorem Th33: :: UPROOTS:33

for b₁ being non empty multLoopStr_0 holds 1_. b₁ = <%(1. b₁)%>

proof end;

theorem Th34: :: UPROOTS:34

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for b₂ being Polynomial of b₁ holds b₂ *' <%(1. b₁)%> = b₂

proof end;

theorem Th35: :: UPROOTS:35

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Polynomial of b₁ st ( len b₂ = 0 or len b₃ = 0 ) holds
len (b₂ *' b₃) = 0

proof end;

theorem Th36: :: UPROOTS:36

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Polynomial of b₁ st b₂ *' b₃ is non-zero holds
( b₂ is non-zero & b₃ is non-zero )

proof end;

theorem Th37: :: UPROOTS:37

for b₁ being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital doubleLoopStr
for b₂, b₃ being Polynomial of b₁ st (b₂ . ((len b₂) -' 1)) * (b₃ . ((len b₃) -' 1)) <> 0. b₁ holds
0 < len (b₂ *' b₃)

proof end;

theorem Th38: :: UPROOTS:38

for b₁ being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital domRing-like doubleLoopStr
for b₂, b₃ being Polynomial of b₁ st 1 < len b₂ & 1 < len b₃ holds
len b₂ < len (b₂ *' b₃)

proof end;

theorem Th39: :: UPROOTS:39

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃ being Element of b₁
for b₄ being Polynomial of b₁ holds
( (<%b₂,b₃%> *' b₄) . 0 = b₂ * (b₄ . 0) & ( for b₅ being Nat holds (<%b₂,b₃%> *' b₄) . (b₅ + 1) = (b₂ * (b₄ . (b₅ + 1))) + (b₃ * (b₄ . b₅)) ) )

proof end;

theorem Th40: :: UPROOTS:40

for b₁ being non empty unital associative commutative add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr
for b₂ being Element of b₁
for b₃ being non-zero Polynomial of b₁ holds len (<%b₂,(1. b₁)%> *' b₃) = (len b₃) + 1

proof end;

theorem Th41: :: UPROOTS:41

for b₁ being non degenerated comRing
for b₂ being Element of b₁
for b₃ being Nat holds len (<%b₂,(1. b₁)%> `^ b₃) = b₃ + 1

proof end;

registration

let c₁ be non degenerated comRing;
let c₂ be Element of c₁;
let c₃ be Nat;
cluster <%a₂,(1. a₁)%> `^ a₃ -> non-zero ;
correctness

proof end;

end;

theorem Th42: :: UPROOTS:42

for b₁ being non degenerated comRing
for b₂ being Element of b₁
for b₃ being non-zero Polynomial of b₁
for b₄ being Nat holds len ((<%b₂,(1. b₁)%> `^ b₄) *' b₃) = b₄ + (len b₃)

proof end;

theorem Th43: :: UPROOTS:43

for b₁ being non empty unital associative commutative add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr
for b₂ being Element of b₁
for b₃, b₄ being Polynomial of b₁ st b₃ = <%b₂,(1. b₁)%> *' b₄ & b₃ . ((len b₃) -' 1) = 1. b₁ holds
b₄ . ((len b₄) -' 1) = 1. b₁

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be Polynomial of c₁;
let c₃ be Nat;
func poly_shift c₂,c₃ -> Polynomial of a₁ means :Def6: :: UPROOTS:def 6
for b₁ being Nat holds a₄ . b₁ = a₂ . (a₃ + b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines poly_shift UPROOTS:def 6 :

theorem Th44: :: UPROOTS:44

for b₁ being non empty ZeroStr
for b₂ being Polynomial of b₁ holds poly_shift b₂,0 = b₂

proof end;

theorem Th45: :: UPROOTS:45

for b₁ being non empty ZeroStr
for b₂ being Nat
for b₃ being Polynomial of b₁ st b₂ >= len b₃ holds
poly_shift b₃,b₂ = 0_. b₁

proof end;

theorem Th46: :: UPROOTS:46

for b₁ being non empty non degenerated multLoopStr_0
for b₂ being Nat
for b₃ being Polynomial of b₁ st b₂ <= len b₃ holds
(len (poly_shift b₃,b₂)) + b₂ = len b₃

proof end;

theorem Th47: :: UPROOTS:47

for b₁ being non degenerated comRing
for b₂ being Element of b₁
for b₃ being Nat
for b₄ being Polynomial of b₁ st b₃ < len b₄ holds
eval (poly_shift b₄,b₃),b₂ = (b₂ * (eval (poly_shift b₄,(b₃ + 1)),b₂)) + (b₄ . b₃)

proof end;

theorem Th48: :: UPROOTS:48

for b₁ being non degenerated comRing
for b₂ being Polynomial of b₁ st len b₂ = 1 holds
Roots b₂ = {}

proof end;

definition

let c₁ be non degenerated comRing;
let c₂ be Element of c₁;
let c₃ be Polynomial of c₁;
assume E50: c₂ is_a_root_of c₃ ;
func poly_quotient c₃,c₂ -> Polynomial of a₁ means :Def7: :: UPROOTS:def 7
( (len a₄) + 1 = len a₃ & ( for b₁ being Nat holds a₄ . b₁ = eval (poly_shift a₃,(b₁ + 1)),a₂ ) ) if len a₃ > 0
otherwise a₄ = 0_. a₁;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def7 defines poly_quotient UPROOTS:def 7 :

theorem Th49: :: UPROOTS:49

for b₁ being non degenerated comRing
for b₂ being Element of b₁
for b₃ being non-zero Polynomial of b₁ st b₂ is_a_root_of b₃ holds
len (poly_quotient b₃,b₂) > 0

proof end;

theorem Th50: :: UPROOTS:50

for b₁ being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂ being Element of b₁ holds Roots <%(- b₂),(1. b₁)%> = {b₂}

proof end;

theorem Th51: :: UPROOTS:51

for b₁ being non trivial comRing
for b₂ being Element of b₁
for b₃, b₄ being Polynomial of b₁ st b₃ = <%(- b₂),(1. b₁)%> *' b₄ holds
b₂ is_a_root_of b₃

proof end;

theorem Th52: :: UPROOTS:52

for b₁ being non degenerated comRing
for b₂ being Element of b₁
for b₃ being Polynomial of b₁ st b₂ is_a_root_of b₃ holds
b₃ = <%(- b₂),(1. b₁)%> *' (poly_quotient b₃,b₂)

proof end;

theorem Th53: :: UPROOTS:53

for b₁ being non degenerated comRing
for b₂ being Element of b₁
for b₃, b₄ being Polynomial of b₁ st b₃ = <%(- b₂),(1. b₁)%> *' b₄ holds
b₂ is_a_root_of b₃

proof end;

E55: now

let c₁ be domRing;
let c₂ be non-zero Polynomial of c₁;
c₂ <> 0_. c₁ by Def5;
then len c₂ <> 0 by POLYNOM4:8;
then len c₂ > 0 ;
then E56: len c₂ >= 0 + 1 by NAT_1:38;
defpred S₁[ Nat] means for b₁ being Polynomial of c₁ st len b₁ = a₁ holds
( Roots b₁ is finite & ex b₂ being Nat st
( b₂ = Card (Roots b₁) & b₂ < len b₁ ) );
E57: S₁[1]

proof

let c₃ be Polynomial of c₁;
assume E58: len c₃ = 1 ;
hence Roots c₃ is finite by Th48;
take 0 ;
thus 0 = Card (Roots c₃) by E58, Th48, CARD_1:78;
thus 0 < len c₃ by E58;

end;

E58: for b₁ being Nat st b₁ >= 1 & S₁[b₁] holds
S₁[b₁ + 1]

proof

let c₃ be Nat;
assume that
E59: c₃ >= 1 and
E60: S₁[c₃] ;
let c₄ be Polynomial of c₁;
assume E61: len c₄ = c₃ + 1 ;
then E62: len c₄ > 1 by E59, NAT_1:38;

per cases ;

suppose c₄ is with_roots ;

then consider c₅ being Element of c₁ such that
E63: c₅ is_a_root_of c₄ by POLYNOM5:def 7;
E64: len c₄ > 0 by E62;
E65: c₄ = <%(- c₅),(1. c₁)%> *' (poly_quotient c₄,c₅) by E63, Th52;
set c₆ = <%(- c₅),(1. c₁)%>;
set c₇ = poly_quotient c₄,c₅;
E66: (len (poly_quotient c₄,c₅)) + 1 = len c₄ by E63, E64, Def7;
then E67: len (poly_quotient c₄,c₅) = c₃ by E61;
then E68: Roots (poly_quotient c₄,c₅) is finite by E60;
E69: Roots <%(- c₅),(1. c₁)%> = {c₅} by Th50;
Roots c₄ = (Roots <%(- c₅),(1. c₁)%>) \/ (Roots (poly_quotient c₄,c₅)) by E65, Th25;
hence Roots c₄ is finite by E68, E69, FINSET_1:14;
consider c₈ being Nat such that
E70: c₈ = Card (Roots (poly_quotient c₄,c₅)) and
E71: c₈ < len (poly_quotient c₄,c₅) by E60, E67;
reconsider c₉ = Roots (poly_quotient c₄,c₅) as finite set by E60, E67;
reconsider c₁₀ = Roots <%(- c₅),(1. c₁)%> as finite set by E69;
reconsider c₁₁ = c₉ \/ c₁₀ as finite set ;
take c₁₂ = card c₁₁;
thus c₁₂ = Card (Roots c₄) by E65, Th25;
card c₁₀ = 1 by E69, CARD_1:79;
then E72: card c₁₁ <= c₈ + 1 by E70, CARD_2:62;
c₈ + 1 < c₃ + 1 by E61, E66, E71, XREAL_1:10;
hence c₁₂ < len c₄ by E61, E72, XREAL_1:2;

end;

suppose E63: not c₄ is with_roots ;

E64: now

assume Roots c₄ <> {} ;
then consider c₅ being set such that
E65: c₅ in Roots c₄ by XBOOLE_0:def 1;
reconsider c₆ = c₅ as Element of c₁ by E65;
c₆ is_a_root_of c₄ by E65, POLYNOM5:def 9;
hence contradiction by E63, POLYNOM5:def 7;

end;

hence Roots c₄ is finite ;
take 0 ;
thus 0 = Card (Roots c₄) by E64, CARD_1:78;
thus 0 < len c₄ by E62;

end;

for b₁ being Nat st b₁ >= 1 holds
S₁[b₁] from INT_2:sch 1(E57, E58);
hence ( Roots c₂ is finite & ex b₁ being Nat st
( b₁ = Card (Roots c₂) & b₁ < len c₂ ) ) by E56;

end;

registration

let c₁ be domRing;
let c₂ be non-zero Polynomial of c₁;
cluster Roots a₂ -> finite ;
correctness by Lemma55;

end;

definition

let c₁ be non degenerated comRing;
let c₂ be Element of c₁;
let c₃ be non-zero Polynomial of c₁;
func multiplicity c₃,c₂ -> Nat means :Def8: :: UPROOTS:def 8
ex b₁ being non empty finite Subset of NAT st
( b₁ = { b₂ where B is Nat : ex b₁ being Polynomial of a₁ st a₃ = (<%(- a₂),(1. a₁)%> `^ b₂) *' b₃ } & a₄ = max b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines multiplicity UPROOTS:def 8 :

theorem Th54: :: UPROOTS:54

for b₁ being non degenerated comRing
for b₂ being non-zero Polynomial of b₁
for b₃ being Element of b₁ holds
( b₃ is_a_root_of b₂ iff multiplicity b₂,b₃ >= 1 )

proof end;

theorem Th55: :: UPROOTS:55

for b₁ being non degenerated comRing
for b₂ being Element of b₁ holds multiplicity <%(- b₂),(1. b₁)%>,b₂ = 1

proof end;

definition

let c₁ be domRing;
let c₂ be non-zero Polynomial of c₁;
func BRoots c₂ -> bag of the carrier of a₁ means :Def9: :: UPROOTS:def 9
( support a₃ = Roots a₂ & ( for b₁ being Element of a₁ holds a₃ . b₁ = multiplicity a₂,b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines BRoots UPROOTS:def 9 :

theorem Th56: :: UPROOTS:56

for b₁ being domRing
for b₂ being Element of b₁ holds BRoots <%(- b₂),(1. b₁)%> = {b₂},1 -bag

proof end;

theorem Th57: :: UPROOTS:57

for b₁ being domRing
for b₂ being Element of b₁
for b₃, b₄ being non-zero Polynomial of b₁ holds multiplicity (b₃ *' b₄),b₂ = (multiplicity b₃,b₂) + (multiplicity b₄,b₂)

proof end;

theorem Th58: :: UPROOTS:58

for b₁ being domRing
for b₂, b₃ being non-zero Polynomial of b₁ holds BRoots (b₂ *' b₃) = (BRoots b₂) + (BRoots b₃)

proof end;

E63: now

let c₁ be domRing;
let c₂, c₃ be non-zero Polynomial of c₁;
BRoots (c₂ *' c₃) = (BRoots c₂) + (BRoots c₃) by Th58;
hence degree (BRoots (c₂ *' c₃)) = (degree (BRoots c₂)) + (degree (BRoots c₃)) by Th17;

end;

theorem Th59: :: UPROOTS:59

for b₁ being domRing
for b₂ being non-zero Polynomial of b₁ st len b₂ = 1 holds
degree (BRoots b₂) = 0

proof end;

theorem Th60: :: UPROOTS:60

for b₁ being domRing
for b₂ being Element of b₁
for b₃ being Nat holds degree (BRoots (<%(- b₂),(1. b₁)%> `^ b₃)) = b₃

proof end;

theorem Th61: :: UPROOTS:61

for b₁ being algebraic-closed domRing
for b₂ being non-zero Polynomial of b₁ holds degree (BRoots b₂) = (len b₂) -' 1

proof end;

definition

let c₁ be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let c₂ be Element of c₁;
let c₃ be Nat;
func fpoly_mult_root c₂,c₃ -> FinSequence of (Polynom-Ring a₁) means :Def10: :: UPROOTS:def 10
( len a₄ = a₃ & ( for b₁ being Nat st b₁ in dom a₄ holds
a₄ . b₁ = <%(- a₂),(1. a₁)%> ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines fpoly_mult_root UPROOTS:def 10 :

definition

let c₁ be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let c₂ be bag of the carrier of c₁;
func poly_with_roots c₂ -> Polynomial of a₁ means :Def11: :: UPROOTS:def 11
ex b₁ being FinSequence of the carrier of (Polynom-Ring a₁) * ex b₂ being FinSequence of a₁ st
( len b₁ = card (support a₂) & b₂ = canFS (support a₂) & ( for b₃ being Nat st b₃ in dom b₁ holds
b₁ . b₃ = fpoly_mult_root (b₂ /. b₃),(a₂ . (b₂ /. b₃)) ) & a₃ = Product (FlattenSeq b₁) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines poly_with_roots UPROOTS:def 11 :

theorem Th62: :: UPROOTS:62

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr holds poly_with_roots (EmptyBag the carrier of b₁) = <%(1. b₁)%>

proof end;

theorem Th63: :: UPROOTS:63

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being Element of b₁ holds poly_with_roots ({b₂},1 -bag ) = <%(- b₂),(1. b₁)%>

proof end;

theorem Th64: :: UPROOTS:64

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being bag of the carrier of b₁
for b₃ being FinSequence of the carrier of (Polynom-Ring b₁) *
for b₄ being FinSequence of b₁ st len b₃ = card (support b₂) & b₄ = canFS (support b₂) & ( for b₅ being Nat st b₅ in dom b₃ holds
b₃ . b₅ = fpoly_mult_root (b₄ /. b₅),(b₂ . (b₄ /. b₅)) ) holds
len (FlattenSeq b₃) = degree b₂

proof end;

theorem Th65: :: UPROOTS:65

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being bag of the carrier of b₁
for b₃ being FinSequence of the carrier of (Polynom-Ring b₁) *
for b₄ being FinSequence of b₁
for b₅ being Element of b₁ st len b₃ = card (support b₂) & b₄ = canFS (support b₂) & ( for b₆ being Nat st b₆ in dom b₃ holds
b₃ . b₆ = fpoly_mult_root (b₄ /. b₆),(b₂ . (b₄ /. b₆)) ) holds
( ( b₅ in support b₂ implies card ((FlattenSeq b₃) " {<%(- b₅),(1. b₁)%>}) = b₂ . b₅ ) & ( not b₅ in support b₂ implies card ((FlattenSeq b₃) " {<%(- b₅),(1. b₁)%>}) = 0 ) )

proof end;

theorem Th66: :: UPROOTS:66

for b₁ being comRing
for b₂, b₃ being bag of the carrier of b₁ holds poly_with_roots (b₂ + b₃) = (poly_with_roots b₂) *' (poly_with_roots b₃)

proof end;

theorem Th67: :: UPROOTS:67

for b₁ being algebraic-closed domRing
for b₂ being non-zero Polynomial of b₁ st b₂ . ((len b₂) -' 1) = 1. b₁ holds
b₂ = poly_with_roots (BRoots b₂)

proof end;

theorem Th68: :: UPROOTS:68

for b₁ being comRing
for b₂ being non empty finite Subset of b₁
for b₃ being FinSequence of (Polynom-Ring b₁) st len b₃ = card b₂ & ( for b₄ being Nat
for b₅ being Element of b₁ st b₄ in dom b₃ & b₅ = (canFS b₂) . b₄ holds
b₃ . b₄ = <%(- b₅),(1. b₁)%> ) holds
poly_with_roots (b₂,1 -bag ) = Product b₃

proof end;

theorem Th69: :: UPROOTS:69

for b₁ being non trivial comRing
for b₂ being non empty finite Subset of b₁
for b₃ being Element of b₁
for b₄ being FinSequence of b₁ st len b₄ = card b₂ & ( for b₅ being Nat
for b₆ being Element of b₁ st b₅ in dom b₄ & b₆ = (canFS b₂) . b₅ holds
b₄ . b₅ = eval <%(- b₆),(1. b₁)%>,b₃ ) holds
eval (poly_with_roots (b₂,1 -bag )),b₃ = Product b₄

proof end;