begin
Lm1:
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of L
for G being FinSequence
for k being Nat st G = F | (Seg k) & len F = k + 1 holds
( G is FinSequence of L & dom G c= dom F & len G = k & F = G ^ <*(F /. (k + 1))*> )
theorem Th1:
theorem Th2:
theorem Th3:
Lm2:
( Im (1_ F_Complex ) = 0 & Im (- (1_ F_Complex )) = 0 & Im (0. F_Complex ) = 0 )
Lm3:
for z being Element of F_Complex st Im z = 0 holds
z *' = z
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
begin
Lm4:
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds - (- p) = p
theorem Th9:
Lm5:
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for f being Element of (Polynom-Ring L) st f = p holds
- f = - p
theorem
theorem Th11:
theorem Th12:
:: deftheorem Def1 defines Coeff HURWITZ:def 1 :
theorem Th13:
Lm6:
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L
for p29 being Element of (Polynom-Ring L) st p29 = p2 holds
for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p29 * F)
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
:: deftheorem defines degree HURWITZ:def 2 :
Lm7:
for L being non empty ZeroStr
for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L
theorem Th20:
Lm8:
for L being non empty ZeroStr
for p being Polynomial of L st deg p <> - 1 holds
p . (deg p) <> 0. L
Lm9:
for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )
theorem
Lm10:
for L being non empty ZeroStr
for p being Polynomial of L holds deg p >= - 1
theorem Th22:
theorem Th23:
theorem Th24:
Lm11:
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k <> 0 holds
( ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . 0 = - ((power L) . z,k) & ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . k = 1_ L )
Lm12:
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT
for i being Nat st i <> 0 & i <> k holds
((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . i = 0. L
:: deftheorem defines rpoly HURWITZ:def 3 :
theorem
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
:: deftheorem Def4 defines qpoly HURWITZ:def 4 :
theorem
theorem Th32:
theorem Th33:
begin
:: deftheorem Def5 defines div HURWITZ:def 5 :
:: deftheorem defines mod HURWITZ:def 6 :
:: deftheorem Def7 defines divides HURWITZ:def 7 :
theorem Th34:
theorem
theorem
begin
:: deftheorem Def8 defines Hurwitz HURWITZ:def 8 :
theorem
theorem
theorem Th39:
theorem Th40:
Lm13:
for f, g, h being Polynomial of F_Complex st f = g *' h holds
for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds
x is_a_root_of f
theorem Th41:
:: deftheorem Def9 defines *' HURWITZ:def 9 :
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
Lm14:
for x, xv being Element of COMPLEX
for u, v, uv, vv being Element of REAL st x = u + (v * <i> ) & xv = uv + (vv * <i> ) holds
(|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 ) = (4 * u) * uv
Lm15:
for x, xv being Element of COMPLEX
for u, v, uv, vv being Element of REAL st x = u + (v * <i> ) & xv = uv + (vv * <i> ) & uv < 0 holds
( ( u < 0 implies |.(x - xv).| < |.(x + (xv *' )).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *' )).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *' )).| ) )
theorem Th48:
theorem Th49:
theorem Th50:
:: deftheorem defines F* HURWITZ:def 10 :
theorem Th51:
theorem Th52:
theorem
theorem