:: by Krzysztof Treyderowski and Christoph Schwarzweller

::

:: Received October 12, 2006

:: Copyright (c) 2006-2017 Association of Mizar Users

Lm1: for j being Integer holds

( j >= 0 or j = - 1 or j < - 1 )

proof end;

Lm2: for j being Integer holds

( j >= 1 or j = 0 or j < 0 )

proof end;

theorem Th1: :: POLYNOM8:1

for n being Nat

for L being non empty non degenerated well-unital domRing-like doubleLoopStr

for x being Element of L st x <> 0. L holds

x |^ n <> 0. L

for L being non empty non degenerated well-unital domRing-like doubleLoopStr

for x being Element of L st x <> 0. L holds

x |^ n <> 0. L

proof end;

registration

for b_{1} being non empty right_complementable right-distributive well-unital add-associative right_zeroed associative doubleLoopStr st b_{1} is almost_left_invertible holds

b_{1} is domRing-like
end;

cluster non empty right_complementable almost_left_invertible right-distributive well-unital add-associative right_zeroed associative -> non empty right_complementable right-distributive well-unital add-associative right_zeroed associative domRing-like for doubleLoopStr ;

coherence for b

b

proof end;

theorem Th2: :: POLYNOM8:2

for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for x, y being Element of L st x <> 0. L & y <> 0. L holds

(x * y) " = (x ") * (y ")

for x, y being Element of L st x <> 0. L & y <> 0. L holds

(x * y) " = (x ") * (y ")

proof end;

theorem Th3: :: POLYNOM8:3

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for z, z1 being Element of L st z <> 0. L holds

z1 = (z1 * z) / z

for z, z1 being Element of L st z <> 0. L holds

z1 = (z1 * z) / z

proof end;

theorem Th4: :: POLYNOM8:4

for L being non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr

for m being Element of NAT

for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds

s /. k = 1. L ) holds

Sum s = m * (1. L)

for m being Element of NAT

for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds

s /. k = 1. L ) holds

Sum s = m * (1. L)

proof end;

theorem Th5: :: POLYNOM8:5

for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for s being FinSequence of L

for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

for s being FinSequence of L

for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

proof end;

definition

let L be non empty well-unital doubleLoopStr ;

let m be Element of NAT ;

coherence

m * (1. L) is Element of L ;

end;
let m be Element of NAT ;

coherence

m * (1. L) is Element of L ;

:: deftheorem defines emb POLYNOM8:def 1 :

for L being non empty well-unital doubleLoopStr

for m being Element of NAT holds emb (m,L) = m * (1. L);

for L being non empty well-unital doubleLoopStr

for m being Element of NAT holds emb (m,L) = m * (1. L);

theorem Th6: :: POLYNOM8:6

for L being Field

for m, n, k being Element of NAT st m > 0 & n > 0 holds

for M1 being Matrix of m,n,L

for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)

for m, n, k being Element of NAT st m > 0 & n > 0 holds

for M1 being Matrix of m,n,L

for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2)

proof end;

theorem Th7: :: POLYNOM8:7

for L being non empty ZeroStr

for p being AlgSequence of L

for i being Element of NAT st p . i <> 0. L holds

len p >= i + 1

for p being AlgSequence of L

for i being Element of NAT st p . i <> 0. L holds

len p >= i + 1

proof end;

theorem Th8: :: POLYNOM8:8

for L being non empty ZeroStr

for s being AlgSequence of L st len s > 0 holds

s . ((len s) - 1) <> 0. L

for s being AlgSequence of L st len s > 0 holds

s . ((len s) - 1) <> 0. L

proof end;

theorem Th9: :: POLYNOM8:9

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 len p > 0 & len q > 0 holds

len (p *' q) <= (len p) + (len q)

for p, q being Polynomial of L st len p > 0 & len q > 0 holds

len (p *' q) <= (len p) + (len q)

proof end;

theorem Th10: :: POLYNOM8:10

for L being non empty associative doubleLoopStr

for k, l being Element of L

for seq being sequence of L holds k * (l * seq) = (k * l) * seq

for k, l being Element of L

for seq being sequence of L holds k * (l * seq) = (k * l) * seq

proof end;

definition
end;

registration

let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;

let m1, m2 be AlgSequence of L;

coherence

m1 * m2 is finite-Support

end;
let m1, m2 be AlgSequence of L;

coherence

m1 * m2 is finite-Support

proof end;

theorem Th11: :: POLYNOM8:11

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for m1, m2 being AlgSequence of L holds len (m1 * m2) <= min ((len m1),(len m2))

for m1, m2 being AlgSequence of L holds len (m1 * m2) <= min ((len m1),(len m2))

proof end;

theorem :: POLYNOM8:12

for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr

for m1, m2 being AlgSequence of L st len m1 = len m2 holds

len (m1 * m2) = len m1

for m1, m2 being AlgSequence of L st len m1 = len m2 holds

len (m1 * m2) = len m1

proof end;

definition

let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ;

let a be Element of L;

let i be Integer;

( ( 0 <= i implies (power L) . (a,i) is Element of L ) & ( not 0 <= i implies ((power L) . (a,|.i.|)) " is Element of L ) )

for b_{1} being Element of L holds verum
;

end;
let a be Element of L;

let i be Integer;

func pow (a,i) -> Element of L equals :Def2: :: POLYNOM8:def 3

(power L) . (a,i) if 0 <= i

otherwise ((power L) . (a,|.i.|)) " ;

coherence (power L) . (a,i) if 0 <= i

otherwise ((power L) . (a,|.i.|)) " ;

( ( 0 <= i implies (power L) . (a,i) is Element of L ) & ( not 0 <= i implies ((power L) . (a,|.i.|)) " is Element of L ) )

proof end;

consistency for b

:: deftheorem Def2 defines pow POLYNOM8:def 3 :

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for a being Element of L

for i being Integer holds

( ( 0 <= i implies pow (a,i) = (power L) . (a,i) ) & ( not 0 <= i implies pow (a,i) = ((power L) . (a,|.i.|)) " ) );

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for a being Element of L

for i being Integer holds

( ( 0 <= i implies pow (a,i) = (power L) . (a,i) ) & ( not 0 <= i implies pow (a,i) = ((power L) . (a,|.i.|)) " ) );

theorem Th13: :: POLYNOM8:13

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for x being Element of L holds pow (x,0) = 1. L

for x being Element of L holds pow (x,0) = 1. L

proof end;

Lm3: for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for a being Element of L

for i being Integer st 0 > i holds

pow (a,i) = (pow (a,|.i.|)) "

proof end;

Lm4: for L being non empty non degenerated almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for i being Integer

for x being Element of L st i <= 0 holds

pow (x,i) = (pow (x,|.i.|)) "

proof end;

theorem Th14: :: POLYNOM8:14

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for x being Element of L holds pow (x,1) = x

for x being Element of L holds pow (x,1) = x

proof end;

theorem Th15: :: POLYNOM8:15

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for x being Element of L holds pow (x,(- 1)) = x "

for x being Element of L holds pow (x,(- 1)) = x "

proof end;

Lm5: for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for i being Element of NAT holds pow ((1. L),i) = 1. L

proof end;

theorem Th16: :: POLYNOM8:16

for L being non empty non degenerated almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for i being Integer holds pow ((1. L),i) = 1. L

for i being Integer holds pow ((1. L),i) = 1. L

proof end;

theorem Th17: :: POLYNOM8:17

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for x being Element of L

for n being Element of NAT holds

( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) )

for x being Element of L

for n being Element of NAT holds

( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) )

proof end;

Lm6: for L being non empty well-unital doubleLoopStr

for n being Element of NAT holds (1. L) |^ n = 1. L

proof end;

Lm7: for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for m being Element of NAT

for x being Element of L st x <> 0. L holds

(x |^ m) * ((x ") |^ m) = 1. L

proof end;

theorem Th18: :: POLYNOM8:18

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for i being Integer

for x being Element of L st x <> 0. L holds

(pow (x,i)) " = pow (x,(- i))

for i being Integer

for x being Element of L st x <> 0. L holds

(pow (x,i)) " = pow (x,(- i))

proof end;

theorem Th19: :: POLYNOM8:19

for L being Field

for j being Integer

for x being Element of L st x <> 0. L holds

pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1))

for j being Integer

for x being Element of L st x <> 0. L holds

pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1))

proof end;

theorem Th20: :: POLYNOM8:20

for L being Field

for j being Integer

for x being Element of L st x <> 0. L holds

pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1)))

for j being Integer

for x being Element of L st x <> 0. L holds

pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1)))

proof end;

theorem Th21: :: POLYNOM8:21

for L being Field

for i, j being Integer

for x being Element of L st x <> 0. L holds

(pow (x,i)) * (pow (x,j)) = pow (x,(i + j))

for i, j being Integer

for x being Element of L st x <> 0. L holds

(pow (x,i)) * (pow (x,j)) = pow (x,(i + j))

proof end;

Lm8: for L being non empty non degenerated right_complementable almost_left_invertible left-distributive well-unital add-associative right_zeroed associative commutative doubleLoopStr

for k being Element of NAT

for x being Element of L st x <> 0. L holds

(x ") |^ k = (x |^ k) "

proof end;

theorem Th22: :: POLYNOM8:22

for L being non empty non degenerated right_complementable almost_left_invertible left-distributive well-unital add-associative right_zeroed associative commutative doubleLoopStr

for k being Element of NAT

for x being Element of L st x <> 0. L holds

pow ((x "),k) = pow (x,(- k))

for k being Element of NAT

for x being Element of L st x <> 0. L holds

pow ((x "),k) = pow (x,(- k))

proof end;

theorem Th23: :: POLYNOM8:23

for L being Field

for x being Element of L st x <> 0. L holds

for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1)))

for x being Element of L st x <> 0. L holds

for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1)))

proof end;

theorem Th24: :: POLYNOM8:24

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for x being Element of L

for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m)

for x being Element of L

for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m)

proof end;

Lm9: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for x being Element of L st x <> 0. L holds

for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) "

proof end;

theorem Th25: :: POLYNOM8:25

for L being Field

for x being Element of L st x <> 0. L holds

for i being Integer holds pow ((x "),i) = (pow (x,i)) "

for x being Element of L st x <> 0. L holds

for i being Integer holds pow ((x "),i) = (pow (x,i)) "

proof end;

theorem Th26: :: POLYNOM8:26

for L being Field

for x being Element of L st x <> 0. L holds

for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j)

for x being Element of L st x <> 0. L holds

for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j)

proof end;

theorem Th27: :: POLYNOM8:27

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for x being Element of L

for i, k being Element of NAT st 1 <= k holds

pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))

for x being Element of L

for i, k being Element of NAT st 1 <= k holds

pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))

proof end;

Lm10: for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for x being Element of L

for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds

(x ") |^ m = 1. L

proof end;

Lm11: for L being non empty non degenerated almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for x being Element of L

for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds

x |^ i = 1. L

proof end;

definition

let m be Nat;

let L be non empty ZeroStr ;

let p be AlgSequence of L;

ex b_{1} being Matrix of m,1,L st

for i being Nat st 1 <= i & i <= m holds

b_{1} * (i,1) = p . (i - 1)

for b_{1}, b_{2} being Matrix of m,1,L st ( for i being Nat st 1 <= i & i <= m holds

b_{1} * (i,1) = p . (i - 1) ) & ( for i being Nat st 1 <= i & i <= m holds

b_{2} * (i,1) = p . (i - 1) ) holds

b_{1} = b_{2}

end;
let L be non empty ZeroStr ;

let p be AlgSequence of L;

func mConv (p,m) -> Matrix of m,1,L means :Def3: :: POLYNOM8:def 4

for i being Nat st 1 <= i & i <= m holds

it * (i,1) = p . (i - 1);

existence for i being Nat st 1 <= i & i <= m holds

it * (i,1) = p . (i - 1);

ex b

for i being Nat st 1 <= i & i <= m holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines mConv POLYNOM8:def 4 :

for m being Nat

for L being non empty ZeroStr

for p being AlgSequence of L

for b_{4} being Matrix of m,1,L holds

( b_{4} = mConv (p,m) iff for i being Nat st 1 <= i & i <= m holds

b_{4} * (i,1) = p . (i - 1) );

for m being Nat

for L being non empty ZeroStr

for p being AlgSequence of L

for b

( b

b

theorem Th28: :: POLYNOM8:28

for m being Nat st m > 0 holds

for L being non empty ZeroStr

for p being AlgSequence of L holds

( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds

(mConv (p,m)) * ((i + 1),1) = p . i ) )

for L being non empty ZeroStr

for p being AlgSequence of L holds

( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds

(mConv (p,m)) * ((i + 1),1) = p . i ) )

proof end;

theorem Th29: :: POLYNOM8:29

for m being Nat st m > 0 holds

for L being non empty ZeroStr

for a being AlgSequence of L

for M being Matrix of m,1,L st ( for i being Nat st i < m holds

M * ((i + 1),1) = a . i ) holds

mConv (a,m) = M

for L being non empty ZeroStr

for a being AlgSequence of L

for M being Matrix of m,1,L st ( for i being Nat st i < m holds

M * ((i + 1),1) = a . i ) holds

mConv (a,m) = M

proof end;

definition

let L be non empty ZeroStr ;

let M be Matrix of L;

ex b_{1} being AlgSequence of L st

( ( for i being Nat st i < len M holds

b_{1} . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

b_{1} . i = 0. L ) )

for b_{1}, b_{2} being AlgSequence of L st ( for i being Nat st i < len M holds

b_{1} . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

b_{1} . i = 0. L ) & ( for i being Nat st i < len M holds

b_{2} . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

b_{2} . i = 0. L ) holds

b_{1} = b_{2}

end;
let M be Matrix of L;

func aConv M -> AlgSequence of L means :Def4: :: POLYNOM8:def 5

( ( for i being Nat st i < len M holds

it . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

it . i = 0. L ) );

existence ( ( for i being Nat st i < len M holds

it . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

it . i = 0. L ) );

ex b

( ( for i being Nat st i < len M holds

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem Def4 defines aConv POLYNOM8:def 5 :

for L being non empty ZeroStr

for M being Matrix of L

for b_{3} being AlgSequence of L holds

( b_{3} = aConv M iff ( ( for i being Nat st i < len M holds

b_{3} . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds

b_{3} . i = 0. L ) ) );

for L being non empty ZeroStr

for M being Matrix of L

for b

( b

b

b

definition
end;

:: deftheorem defines is_primitive_root_of_degree POLYNOM8:def 6 :

for L being non empty well-unital doubleLoopStr

for x being Element of L

for n being Element of NAT holds

( x is_primitive_root_of_degree n iff ( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds

x |^ i <> 1. L ) ) );

for L being non empty well-unital doubleLoopStr

for x being Element of L

for n being Element of NAT holds

( x is_primitive_root_of_degree n iff ( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds

x |^ i <> 1. L ) ) );

theorem Th30: :: POLYNOM8:30

for L being non empty non degenerated right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr

for n being Element of NAT holds not 0. L is_primitive_root_of_degree n

for n being Element of NAT holds not 0. L is_primitive_root_of_degree n

proof end;

theorem Th31: :: POLYNOM8:31

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for m being Element of NAT

for x being Element of L st x is_primitive_root_of_degree m holds

x " is_primitive_root_of_degree m

for m being Element of NAT

for x being Element of L st x is_primitive_root_of_degree m holds

x " is_primitive_root_of_degree m

proof end;

theorem Th32: :: POLYNOM8:32

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for m being Element of NAT

for x being Element of L st x is_primitive_root_of_degree m holds

for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds

pow (x,(i - j)) <> 1. L

for m being Element of NAT

for x being Element of L st x is_primitive_root_of_degree m holds

for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds

pow (x,(i - j)) <> 1. L

proof end;

definition

let m be Nat;

let L be non empty well-unital doubleLoopStr ;

let p be Polynomial of L;

let x be Element of L;

ex b_{1} being AlgSequence of L st

( ( for i being Nat st i < m holds

b_{1} . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

b_{1} . i = 0. L ) )

for b_{1}, b_{2} being AlgSequence of L st ( for i being Nat st i < m holds

b_{1} . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

b_{1} . i = 0. L ) & ( for i being Nat st i < m holds

b_{2} . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

b_{2} . i = 0. L ) holds

b_{1} = b_{2}

end;
let L be non empty well-unital doubleLoopStr ;

let p be Polynomial of L;

let x be Element of L;

func DFT (p,x,m) -> AlgSequence of L means :Def6: :: POLYNOM8:def 7

( ( for i being Nat st i < m holds

it . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

it . i = 0. L ) );

existence ( ( for i being Nat st i < m holds

it . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

it . i = 0. L ) );

ex b

( ( for i being Nat st i < m holds

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem Def6 defines DFT POLYNOM8:def 7 :

for m being Nat

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L

for x being Element of L

for b_{5} being AlgSequence of L holds

( b_{5} = DFT (p,x,m) iff ( ( for i being Nat st i < m holds

b_{5} . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

b_{5} . i = 0. L ) ) );

for m being Nat

for L being non empty well-unital doubleLoopStr

for p being Polynomial of L

for x being Element of L

for b

( b

b

b

theorem Th33: :: POLYNOM8:33

for m being Nat

for L being non empty well-unital doubleLoopStr

for x being Element of L holds DFT ((0_. L),x,m) = 0_. L

for L being non empty well-unital doubleLoopStr

for x being Element of L holds DFT ((0_. L),x,m) = 0_. L

proof end;

theorem Th34: :: POLYNOM8:34

for m being Nat

for L being Field

for p, q being Polynomial of L

for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m)

for L being Field

for p, q being Polynomial of L

for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m)

proof end;

definition

let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ;

let m be Nat;

let x be Element of L;

ex b_{1} being Matrix of m,L st

for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

b_{1} * (i,j) = pow (x,((i - 1) * (j - 1)))

for b_{1}, b_{2} being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

b_{1} * (i,j) = pow (x,((i - 1) * (j - 1))) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

b_{2} * (i,j) = pow (x,((i - 1) * (j - 1))) ) holds

b_{1} = b_{2}

end;
let m be Nat;

let x be Element of L;

func Vandermonde (x,m) -> Matrix of m,L means :Def7: :: POLYNOM8:def 8

for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

it * (i,j) = pow (x,((i - 1) * (j - 1)));

existence for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

it * (i,j) = pow (x,((i - 1) * (j - 1)));

ex b

for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines Vandermonde POLYNOM8:def 8 :

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for m being Nat

for x being Element of L

for b_{4} being Matrix of m,L holds

( b_{4} = Vandermonde (x,m) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

b_{4} * (i,j) = pow (x,((i - 1) * (j - 1))) );

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr

for m being Nat

for x being Element of L

for b

( b

b

notation

let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ;

let m be Nat;

let x be Element of L;

synonym VM (x,m) for Vandermonde (x,m);

end;
let m be Nat;

let x be Element of L;

synonym VM (x,m) for Vandermonde (x,m);

theorem Th35: :: POLYNOM8:35

for L being Field

for m, n being Nat st m > 0 holds

for M being Matrix of m,n,L holds (1. (L,m)) * M = M

for m, n being Nat st m > 0 holds

for M being Matrix of m,n,L holds (1. (L,m)) * M = M

proof end;

theorem Th36: :: POLYNOM8:36

for L being Field

for m being Element of NAT st 0 < m holds

for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds

u * v = (emb (m,L)) * u1

for m being Element of NAT st 0 < m holds

for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds

(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds

u * v = (emb (m,L)) * u1

proof end;

Lm12: for L being Field

for m being Element of NAT st m > 0 holds

for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))

proof end;

theorem Th37: :: POLYNOM8:37

for L being Field

for x being Element of L

for s being FinSequence of L

for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds

s /. k = pow (x,((i - j) * (k - 1))) ) holds

((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s

for x being Element of L

for s being FinSequence of L

for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds

s /. k = pow (x,((i - j) * (k - 1))) ) holds

((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s

proof end;

theorem Th38: :: POLYNOM8:38

for L being Field

for m, i, j being Element of NAT

for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds

((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L

for m, i, j being Element of NAT

for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds

((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L

proof end;

theorem Th39: :: POLYNOM8:39

for L being Field

for m being Element of NAT st m > 0 holds

for x being Element of L st x is_primitive_root_of_degree m holds

(VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m))

for m being Element of NAT st m > 0 holds

for x being Element of L st x is_primitive_root_of_degree m holds

(VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m))

proof end;

theorem Th40: :: POLYNOM8:40

for L being Field

for m being Element of NAT

for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds

(VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))

for m being Element of NAT

for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds

(VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))

proof end;

theorem Th41: :: POLYNOM8:41

for L being Field

for p being Polynomial of L

for m being Element of NAT st m > 0 & len p <= m holds

for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

for p being Polynomial of L

for m being Element of NAT st m > 0 & len p <= m holds

for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

proof end;

theorem Th42: :: POLYNOM8:42

for L being Field

for p being Polynomial of L

for m being Nat st 0 < m & len p <= m holds

for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

for p being Polynomial of L

for m being Nat st 0 < m & len p <= m holds

for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))

proof end;

theorem Th43: :: POLYNOM8:43

for L being Field

for p, q being Polynomial of L

for m being Element of NAT st m > 0 & len p <= m & len q <= m holds

for x being Element of L st x is_primitive_root_of_degree 2 * m holds

DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)

for p, q being Polynomial of L

for m being Element of NAT st m > 0 & len p <= m & len q <= m holds

for x being Element of L st x is_primitive_root_of_degree 2 * m holds

DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)

proof end;

:: Multiplication of Polynomials using Discrete Fourier Transformation

theorem :: POLYNOM8:44

for L being Field

for p, q being Polynomial of L

for m being Element of NAT st m > 0 & len p <= m & len q <= m holds

for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds

((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q

for p, q being Polynomial of L

for m being Element of NAT st m > 0 & len p <= m & len q <= m holds

for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds

((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q

proof end;