:: by Xiaopeng Yue and Xiquan Liang

::

:: Received August 26, 2008

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

Lm1: for n being Element of NAT

for k being Nat st k <= n & k >= 1 holds

(k - 1) mod n = k - 1

proof end;

Lm2: for n, i, j being Nat st i in Seg n & j in Seg n holds

((j - i) mod n) + 1 in Seg n

proof end;

Lm3: for n, i, j being Nat st ( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] ) holds

((j - i) mod n) + 1 in Seg n

proof end;

:: deftheorem defines is_line_circulant_about MATRIX16:def 1 :

for K being set

for M being Matrix of K

for p being FinSequence holds

( M is_line_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = p . (((j - i) mod (len p)) + 1) ) ) );

for K being set

for M being Matrix of K

for p being FinSequence holds

( M is_line_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = p . (((j - i) mod (len p)) + 1) ) ) );

definition

let K be set ;

let M be Matrix of K;

end;
let M be Matrix of K;

attr M is line_circulant means :: MATRIX16:def 2

ex p being FinSequence of K st

( len p = width M & M is_line_circulant_about p );

ex p being FinSequence of K st

( len p = width M & M is_line_circulant_about p );

:: deftheorem defines line_circulant MATRIX16:def 2 :

for K being set

for M being Matrix of K holds

( M is line_circulant iff ex p being FinSequence of K st

( len p = width M & M is_line_circulant_about p ) );

for K being set

for M being Matrix of K holds

( M is line_circulant iff ex p being FinSequence of K st

( len p = width M & M is_line_circulant_about p ) );

definition

let K be non empty set ;

let p be FinSequence of K;

end;
let p be FinSequence of K;

attr p is first-line-of-circulant means :: MATRIX16:def 3

ex M being Matrix of len p,K st M is_line_circulant_about p;

ex M being Matrix of len p,K st M is_line_circulant_about p;

:: deftheorem defines first-line-of-circulant MATRIX16:def 3 :

for K being non empty set

for p being FinSequence of K holds

( p is first-line-of-circulant iff ex M being Matrix of len p,K st M is_line_circulant_about p );

for K being non empty set

for p being FinSequence of K holds

( p is first-line-of-circulant iff ex M being Matrix of len p,K st M is_line_circulant_about p );

:: deftheorem defines is_col_circulant_about MATRIX16:def 4 :

for K being set

for M being Matrix of K

for p being FinSequence holds

( M is_col_circulant_about p iff ( len p = len M & ( for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = p . (((i - j) mod (len p)) + 1) ) ) );

for K being set

for M being Matrix of K

for p being FinSequence holds

( M is_col_circulant_about p iff ( len p = len M & ( for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = p . (((i - j) mod (len p)) + 1) ) ) );

definition

let K be set ;

let M be Matrix of K;

end;
let M be Matrix of K;

attr M is col_circulant means :: MATRIX16:def 5

ex p being FinSequence of K st

( len p = len M & M is_col_circulant_about p );

ex p being FinSequence of K st

( len p = len M & M is_col_circulant_about p );

:: deftheorem defines col_circulant MATRIX16:def 5 :

for K being set

for M being Matrix of K holds

( M is col_circulant iff ex p being FinSequence of K st

( len p = len M & M is_col_circulant_about p ) );

for K being set

for M being Matrix of K holds

( M is col_circulant iff ex p being FinSequence of K st

( len p = len M & M is_col_circulant_about p ) );

definition

let K be non empty set ;

let p be FinSequence of K;

end;
let p be FinSequence of K;

attr p is first-col-of-circulant means :: MATRIX16:def 6

ex M being Matrix of len p,K st M is_col_circulant_about p;

ex M being Matrix of len p,K st M is_col_circulant_about p;

:: deftheorem defines first-col-of-circulant MATRIX16:def 6 :

for K being non empty set

for p being FinSequence of K holds

( p is first-col-of-circulant iff ex M being Matrix of len p,K st M is_col_circulant_about p );

for K being non empty set

for p being FinSequence of K holds

( p is first-col-of-circulant iff ex M being Matrix of len p,K st M is_col_circulant_about p );

definition

let K be non empty set ;

let p be FinSequence of K;

assume A1: p is first-line-of-circulant ;

existence

ex b_{1} being Matrix of len p,K st b_{1} is_line_circulant_about p
by A1;

uniqueness

for b_{1}, b_{2} being Matrix of len p,K st b_{1} is_line_circulant_about p & b_{2} is_line_circulant_about p holds

b_{1} = b_{2}

end;
let p be FinSequence of K;

assume A1: p is first-line-of-circulant ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def7 defines LCirc MATRIX16:def 7 :

for K being non empty set

for p being FinSequence of K st p is first-line-of-circulant holds

for b_{3} being Matrix of len p,K holds

( b_{3} = LCirc p iff b_{3} is_line_circulant_about p );

for K being non empty set

for p being FinSequence of K st p is first-line-of-circulant holds

for b

( b

definition

let K be non empty set ;

let p be FinSequence of K;

assume A1: p is first-col-of-circulant ;

existence

ex b_{1} being Matrix of len p,K st b_{1} is_col_circulant_about p
by A1;

uniqueness

for b_{1}, b_{2} being Matrix of len p,K st b_{1} is_col_circulant_about p & b_{2} is_col_circulant_about p holds

b_{1} = b_{2}

end;
let p be FinSequence of K;

assume A1: p is first-col-of-circulant ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def8 defines CCirc MATRIX16:def 8 :

for K being non empty set

for p being FinSequence of K st p is first-col-of-circulant holds

for b_{3} being Matrix of len p,K holds

( b_{3} = CCirc p iff b_{3} is_col_circulant_about p );

for K being non empty set

for p being FinSequence of K st p is first-col-of-circulant holds

for b

( b

registration

let K be Field;

ex b_{1} being FinSequence of K st

( b_{1} is first-line-of-circulant & b_{1} is first-col-of-circulant )

end;
cluster Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like first-line-of-circulant first-col-of-circulant for FinSequence of the carrier of K;

existence ex b

( b

proof end;

registration

let K be Field;

let n be Element of NAT ;

coherence

( 0. (K,n) is line_circulant & 0. (K,n) is col_circulant )

end;
let n be Element of NAT ;

coherence

( 0. (K,n) is line_circulant & 0. (K,n) is col_circulant )

proof end;

registration

let K be Field;

let n be Element of NAT ;

let a be Element of K;

coherence

for b_{1} being Matrix of n,K st b_{1} = (n,n) --> a holds

b_{1} is line_circulant

for b_{1} being Matrix of n,K st b_{1} = (n,n) --> a holds

b_{1} is col_circulant

end;
let n be Element of NAT ;

let a be Element of K;

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let K be Field;

ex b_{1} being Matrix of K st

( b_{1} is line_circulant & b_{1} is col_circulant )

end;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V104() tabular line_circulant col_circulant for FinSequence of the carrier of K * ;

existence ex b

( b

proof end;

theorem :: MATRIX16:3

for n being Element of NAT

for D being non empty set

for A being Matrix of n,D st A is line_circulant & n > 0 holds

A @ is col_circulant

for D being non empty set

for A being Matrix of n,D st A is line_circulant & n > 0 holds

A @ is col_circulant

proof end;

theorem :: MATRIX16:4

for n being Element of NAT

for D being non empty set

for t being FinSequence of D

for A being Matrix of n,D st A is_line_circulant_about t & n > 0 holds

t = Line (A,1)

for D being non empty set

for t being FinSequence of D

for A being Matrix of n,D st A is_line_circulant_about t & n > 0 holds

t = Line (A,1)

proof end;

theorem :: MATRIX16:5

for i, j, k, n, l being Element of NAT

for D being non empty set

for A being Matrix of n,D st A is line_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds

A * (i,j) = A * (k,l)

for D being non empty set

for A being Matrix of n,D st A is line_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds

A * (i,j) = A * (k,l)

proof end;

theorem Th6: :: MATRIX16:6

for n being Element of NAT

for K being Field

for a being Element of K

for M1 being Matrix of n,K st M1 is line_circulant holds

a * M1 is line_circulant

for K being Field

for a being Element of K

for M1 being Matrix of n,K st M1 is line_circulant holds

a * M1 is line_circulant

proof end;

theorem Th7: :: MATRIX16:7

for n being Element of NAT

for K being Field

for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds

M1 + M2 is line_circulant

for K being Field

for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds

M1 + M2 is line_circulant

proof end;

theorem Th8: :: MATRIX16:8

for n being Element of NAT

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

(M1 + M2) + M3 is line_circulant

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

(M1 + M2) + M3 is line_circulant

proof end;

theorem :: MATRIX16:9

for n being Element of NAT

for K being Field

for a, b being Element of K

for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds

(a * M1) + (b * M2) is line_circulant

for K being Field

for a, b being Element of K

for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds

(a * M1) + (b * M2) is line_circulant

proof end;

theorem :: MATRIX16:10

for n being Element of NAT

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

((a * M1) + (b * M2)) + (c * M3) is line_circulant

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

((a * M1) + (b * M2)) + (c * M3) is line_circulant

proof end;

theorem Th11: :: MATRIX16:11

for n being Element of NAT

for K being Field

for M1 being Matrix of n,K st M1 is line_circulant holds

- M1 is line_circulant

for K being Field

for M1 being Matrix of n,K st M1 is line_circulant holds

- M1 is line_circulant

proof end;

theorem :: MATRIX16:12

for n being Element of NAT

for K being Field

for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds

M1 - M2 is line_circulant

for K being Field

for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds

M1 - M2 is line_circulant

proof end;

theorem Th13: :: MATRIX16:13

for n being Element of NAT

for K being Field

for a, b being Element of K

for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds

(a * M1) - (b * M2) is line_circulant

for K being Field

for a, b being Element of K

for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds

(a * M1) - (b * M2) is line_circulant

proof end;

theorem :: MATRIX16:14

for n being Element of NAT

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

((a * M1) + (b * M2)) - (c * M3) is line_circulant

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

((a * M1) + (b * M2)) - (c * M3) is line_circulant

proof end;

theorem :: MATRIX16:15

for n being Element of NAT

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

((a * M1) - (b * M2)) - (c * M3) is line_circulant

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

((a * M1) - (b * M2)) - (c * M3) is line_circulant

proof end;

theorem :: MATRIX16:16

for n being Element of NAT

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

((a * M1) - (b * M2)) + (c * M3) is line_circulant

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds

((a * M1) - (b * M2)) + (c * M3) is line_circulant

proof end;

theorem :: MATRIX16:17

for n being Element of NAT

for D being non empty set

for A being Matrix of n,D st A is col_circulant & n > 0 holds

A @ is line_circulant

for D being non empty set

for A being Matrix of n,D st A is col_circulant & n > 0 holds

A @ is line_circulant

proof end;

theorem :: MATRIX16:18

for n being Element of NAT

for D being non empty set

for t being FinSequence of D

for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds

t = Col (A,1)

for D being non empty set

for t being FinSequence of D

for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds

t = Col (A,1)

proof end;

theorem :: MATRIX16:19

for i, j, k, n, l being Element of NAT

for D being non empty set

for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds

A * (i,j) = A * (k,l)

for D being non empty set

for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds

A * (i,j) = A * (k,l)

proof end;

theorem Th20: :: MATRIX16:20

for n being Element of NAT

for K being Field

for a being Element of K

for M1 being Matrix of n,K st M1 is col_circulant holds

a * M1 is col_circulant

for K being Field

for a being Element of K

for M1 being Matrix of n,K st M1 is col_circulant holds

a * M1 is col_circulant

proof end;

theorem Th21: :: MATRIX16:21

for n being Element of NAT

for K being Field

for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds

M1 + M2 is col_circulant

for K being Field

for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds

M1 + M2 is col_circulant

proof end;

theorem Th22: :: MATRIX16:22

for n being Element of NAT

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

(M1 + M2) + M3 is col_circulant

for K being Field

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

(M1 + M2) + M3 is col_circulant

proof end;

theorem :: MATRIX16:23

for n being Element of NAT

for K being Field

for a, b being Element of K

for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds

(a * M1) + (b * M2) is col_circulant

for K being Field

for a, b being Element of K

for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds

(a * M1) + (b * M2) is col_circulant

proof end;

theorem :: MATRIX16:24

for n being Element of NAT

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

((a * M1) + (b * M2)) + (c * M3) is col_circulant

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

((a * M1) + (b * M2)) + (c * M3) is col_circulant

proof end;

theorem Th25: :: MATRIX16:25

for n being Element of NAT

for K being Field

for M1 being Matrix of n,K st M1 is col_circulant holds

- M1 is col_circulant

for K being Field

for M1 being Matrix of n,K st M1 is col_circulant holds

- M1 is col_circulant

proof end;

theorem :: MATRIX16:26

for n being Element of NAT

for K being Field

for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds

M1 - M2 is col_circulant

for K being Field

for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds

M1 - M2 is col_circulant

proof end;

theorem Th27: :: MATRIX16:27

for n being Element of NAT

for K being Field

for a, b being Element of K

for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds

(a * M1) - (b * M2) is col_circulant

for K being Field

for a, b being Element of K

for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds

(a * M1) - (b * M2) is col_circulant

proof end;

theorem :: MATRIX16:28

for n being Element of NAT

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

((a * M1) + (b * M2)) - (c * M3) is col_circulant

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

((a * M1) + (b * M2)) - (c * M3) is col_circulant

proof end;

theorem :: MATRIX16:29

for n being Element of NAT

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

((a * M1) - (b * M2)) - (c * M3) is col_circulant

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

((a * M1) - (b * M2)) - (c * M3) is col_circulant

proof end;

theorem :: MATRIX16:30

for n being Element of NAT

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

((a * M1) - (b * M2)) + (c * M3) is col_circulant

for K being Field

for a, b, c being Element of K

for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds

((a * M1) - (b * M2)) + (c * M3) is col_circulant

proof end;

theorem Th31: :: MATRIX16:31

for K being Field

for p being FinSequence of K st p is first-line-of-circulant holds

- p is first-line-of-circulant

for p being FinSequence of K st p is first-line-of-circulant holds

- p is first-line-of-circulant

proof end;

theorem :: MATRIX16:32

for K being Field

for p being FinSequence of K st p is first-line-of-circulant holds

LCirc (- p) = - (LCirc p)

for p being FinSequence of K st p is first-line-of-circulant holds

LCirc (- p) = - (LCirc p)

proof end;

theorem Th33: :: MATRIX16:33

for K being Field

for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds

p + q is first-line-of-circulant

for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds

p + q is first-line-of-circulant

proof end;

theorem Th34: :: MATRIX16:34

for K being Field

for p, q being FinSequence of K st len p = len q & p is first-line-of-circulant & q is first-line-of-circulant holds

LCirc (p + q) = (LCirc p) + (LCirc q)

for p, q being FinSequence of K st len p = len q & p is first-line-of-circulant & q is first-line-of-circulant holds

LCirc (p + q) = (LCirc p) + (LCirc q)

proof end;

theorem Th35: :: MATRIX16:35

for K being Field

for p being FinSequence of K st p is first-col-of-circulant holds

- p is first-col-of-circulant

for p being FinSequence of K st p is first-col-of-circulant holds

- p is first-col-of-circulant

proof end;

theorem :: MATRIX16:36

for K being Field

for p being FinSequence of K st p is first-col-of-circulant holds

CCirc (- p) = - (CCirc p)

for p being FinSequence of K st p is first-col-of-circulant holds

CCirc (- p) = - (CCirc p)

proof end;

theorem Th37: :: MATRIX16:37

for K being Field

for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds

p + q is first-col-of-circulant

for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds

p + q is first-col-of-circulant

proof end;

theorem Th38: :: MATRIX16:38

for K being Field

for p, q being FinSequence of K st len p = len q & p is first-col-of-circulant & q is first-col-of-circulant holds

CCirc (p + q) = (CCirc p) + (CCirc q)

for p, q being FinSequence of K st len p = len q & p is first-col-of-circulant & q is first-col-of-circulant holds

CCirc (p + q) = (CCirc p) + (CCirc q)

proof end;

theorem Th41: :: MATRIX16:41

for K being Field

for a being Element of K

for p being FinSequence of K st p is first-line-of-circulant holds

a * p is first-line-of-circulant

for a being Element of K

for p being FinSequence of K st p is first-line-of-circulant holds

a * p is first-line-of-circulant

proof end;

theorem Th42: :: MATRIX16:42

for K being Field

for a being Element of K

for p being FinSequence of K st p is first-line-of-circulant holds

LCirc (a * p) = a * (LCirc p)

for a being Element of K

for p being FinSequence of K st p is first-line-of-circulant holds

LCirc (a * p) = a * (LCirc p)

proof end;

theorem :: MATRIX16:43

for K being Field

for a, b being Element of K

for p being FinSequence of K st p is first-line-of-circulant holds

(a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)

for a, b being Element of K

for p being FinSequence of K st p is first-line-of-circulant holds

(a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)

proof end;

theorem :: MATRIX16:44

for K being Field

for a being Element of K

for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds

(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))

for a being Element of K

for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds

(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))

proof end;

theorem :: MATRIX16:45

for K being Field

for a, b being Element of K

for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds

(a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q))

for a, b being Element of K

for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds

(a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q))

proof end;

theorem Th46: :: MATRIX16:46

for K being Field

for a being Element of K

for p being FinSequence of K st p is first-col-of-circulant holds

a * p is first-col-of-circulant

for a being Element of K

for p being FinSequence of K st p is first-col-of-circulant holds

a * p is first-col-of-circulant

proof end;

theorem Th47: :: MATRIX16:47

for K being Field

for a being Element of K

for p being FinSequence of K st p is first-col-of-circulant holds

CCirc (a * p) = a * (CCirc p)

for a being Element of K

for p being FinSequence of K st p is first-col-of-circulant holds

CCirc (a * p) = a * (CCirc p)

proof end;

theorem :: MATRIX16:48

for K being Field

for a, b being Element of K

for p being FinSequence of K st p is first-col-of-circulant holds

(a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p)

for a, b being Element of K

for p being FinSequence of K st p is first-col-of-circulant holds

(a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p)

proof end;

theorem :: MATRIX16:49

for K being Field

for a being Element of K

for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 holds

(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))

for a being Element of K

for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 holds

(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))

proof end;

theorem :: MATRIX16:50

for K being Field

for a, b being Element of K

for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds

(a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))

for a, b being Element of K

for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds

(a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))

proof end;

:: deftheorem defines is_anti-circular_about MATRIX16:def 9 :

for K being Field

for M1 being Matrix of K

for p being FinSequence of K holds

( M1 is_anti-circular_about p iff ( len p = width M1 & ( for i, j being Nat st [i,j] in Indices M1 & i <= j holds

M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) & ( for i, j being Nat st [i,j] in Indices M1 & i >= j holds

M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) ) );

for K being Field

for M1 being Matrix of K

for p being FinSequence of K holds

( M1 is_anti-circular_about p iff ( len p = width M1 & ( for i, j being Nat st [i,j] in Indices M1 & i <= j holds

M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) & ( for i, j being Nat st [i,j] in Indices M1 & i >= j holds

M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) ) );

definition

let K be Field;

let M be Matrix of K;

end;
let M be Matrix of K;

attr M is anti-circular means :: MATRIX16:def 10

ex p being FinSequence of K st

( len p = width M & M is_anti-circular_about p );

ex p being FinSequence of K st

( len p = width M & M is_anti-circular_about p );

:: deftheorem defines anti-circular MATRIX16:def 10 :

for K being Field

for M being Matrix of K holds

( M is anti-circular iff ex p being FinSequence of K st

( len p = width M & M is_anti-circular_about p ) );

for K being Field

for M being Matrix of K holds

( M is anti-circular iff ex p being FinSequence of K st

( len p = width M & M is_anti-circular_about p ) );

definition

let K be Field;

let p be FinSequence of K;

end;
let p be FinSequence of K;

attr p is first-line-of-anti-circular means :: MATRIX16:def 11

ex M being Matrix of len p,K st M is_anti-circular_about p;

ex M being Matrix of len p,K st M is_anti-circular_about p;

:: deftheorem defines first-line-of-anti-circular MATRIX16:def 11 :

for K being Field

for p being FinSequence of K holds

( p is first-line-of-anti-circular iff ex M being Matrix of len p,K st M is_anti-circular_about p );

for K being Field

for p being FinSequence of K holds

( p is first-line-of-anti-circular iff ex M being Matrix of len p,K st M is_anti-circular_about p );

definition

let K be Field;

let p be FinSequence of K;

assume A1: p is first-line-of-anti-circular ;

existence

ex b_{1} being Matrix of len p,K st b_{1} is_anti-circular_about p
by A1;

uniqueness

for b_{1}, b_{2} being Matrix of len p,K st b_{1} is_anti-circular_about p & b_{2} is_anti-circular_about p holds

b_{1} = b_{2}

end;
let p be FinSequence of K;

assume A1: p is first-line-of-anti-circular ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def12 defines ACirc MATRIX16:def 12 :

for K being Field

for p being FinSequence of K st p is first-line-of-anti-circular holds

for b_{3} being Matrix of len p,K holds

( b_{3} = ACirc p iff b_{3} is_anti-circular_about p );

for K being Field

for p being FinSequence of K st p is first-line-of-anti-circular holds

for b

( b

theorem :: MATRIX16:51

for n being Element of NAT

for K being Field

for a being Element of K

for M1 being Matrix of n,K st M1 is anti-circular holds

a * M1 is anti-circular

for K being Field

for a being Element of K

for M1 being Matrix of n,K st M1 is anti-circular holds

a * M1 is anti-circular

proof end;

theorem Th52: :: MATRIX16:52

for n being Element of NAT

for K being Field

for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds

M1 + M2 is anti-circular

for K being Field

for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds

M1 + M2 is anti-circular

proof end;

theorem :: MATRIX16:53

for K being Fanoian Field

for n, i, j being Nat

for M1 being Matrix of n,K st [i,j] in Indices M1 & i = j & M1 is anti-circular holds

M1 * (i,j) = 0. K

for n, i, j being Nat

for M1 being Matrix of n,K st [i,j] in Indices M1 & i = j & M1 is anti-circular holds

M1 * (i,j) = 0. K

proof end;

theorem :: MATRIX16:54

for i, j, k, n, l being Element of NAT

for K being Field

for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds

M1 * (k,l) = M1 * (i,j)

for K being Field

for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds

M1 * (k,l) = M1 * (i,j)

proof end;

theorem Th55: :: MATRIX16:55

for n being Element of NAT

for K being Field

for M1 being Matrix of n,K st M1 is anti-circular holds

- M1 is anti-circular

for K being Field

for M1 being Matrix of n,K st M1 is anti-circular holds

- M1 is anti-circular

proof end;

theorem :: MATRIX16:56

for n being Element of NAT

for K being Field

for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds

M1 - M2 is anti-circular

for K being Field

for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds

M1 - M2 is anti-circular

proof end;

theorem :: MATRIX16:57

for n being Element of NAT

for K being Field

for p being FinSequence of K

for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds

p = Line (M1,1)

for K being Field

for p being FinSequence of K

for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds

p = Line (M1,1)

proof end;

theorem Th58: :: MATRIX16:58

for K being Field

for p being FinSequence of K st p is first-line-of-anti-circular holds

- p is first-line-of-anti-circular

for p being FinSequence of K st p is first-line-of-anti-circular holds

- p is first-line-of-anti-circular

proof end;

theorem :: MATRIX16:59

for K being Field

for p being FinSequence of K st p is first-line-of-anti-circular holds

ACirc (- p) = - (ACirc p)

for p being FinSequence of K st p is first-line-of-anti-circular holds

ACirc (- p) = - (ACirc p)

proof end;

theorem Th60: :: MATRIX16:60

for K being Field

for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds

p + q is first-line-of-anti-circular

for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds

p + q is first-line-of-anti-circular

proof end;

theorem Th61: :: MATRIX16:61

for K being Field

for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds

ACirc (p + q) = (ACirc p) + (ACirc q)

for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds

ACirc (p + q) = (ACirc p) + (ACirc q)

proof end;

theorem Th62: :: MATRIX16:62

for K being Field

for a being Element of K

for p being FinSequence of K st p is first-line-of-anti-circular holds

a * p is first-line-of-anti-circular

for a being Element of K

for p being FinSequence of K st p is first-line-of-anti-circular holds

a * p is first-line-of-anti-circular

proof end;

theorem Th63: :: MATRIX16:63

for K being Field

for a being Element of K

for p being FinSequence of K st p is first-line-of-anti-circular holds

ACirc (a * p) = a * (ACirc p)

for a being Element of K

for p being FinSequence of K st p is first-line-of-anti-circular holds

ACirc (a * p) = a * (ACirc p)

proof end;

theorem :: MATRIX16:64

for K being Field

for a, b being Element of K

for p being FinSequence of K st p is first-line-of-anti-circular holds

(a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)

for a, b being Element of K

for p being FinSequence of K st p is first-line-of-anti-circular holds

(a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)

proof end;

theorem :: MATRIX16:65

for K being Field

for a being Element of K

for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds

(a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))

for a being Element of K

for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds

(a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))

proof end;

theorem :: MATRIX16:66

for K being Field

for a, b being Element of K

for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds

(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))

for a, b being Element of K

for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds

(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))

proof end;

registration
end;