:: Basic Properties of Circulant Matrices and Anti-circular Matrices
:: by Xiaopeng Yue and Xiquan Liang
::
:: Received August 26, 2008
:: Copyright (c) 2008-2021 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;

theorem :: MATRIX16:1

for K being Field
for p being FinSequence of K holds (1_ K) * p = p

proof end;

theorem :: MATRIX16:2

for K being Field
for p being FinSequence of K holds (- (1_ K)) * p = - p

proof end;

definition

let K be set ;
let M be Matrix of K;
let p be FinSequence;

pred M is_line_circulant_about p means :: MATRIX16:def 1
( 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) ) );

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) ) ) );

definition

let K be set ;
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 );

end;

:: 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 ) );

definition

let K be non empty set ;
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;

end;

:: 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 );

definition

let K be set ;
let M be Matrix of K;
let p be FinSequence;

pred M is_col_circulant_about p means :: MATRIX16:def 4
( 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) ) );

end;

:: 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) ) ) );

definition

let K be set ;
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 );

end;

:: 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 ) );

definition

let K be non empty set ;
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;

end;

:: 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 );

definition

let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-line-of-circulant ;

func LCirc p -> Matrix of len p,K means :Def7: :: MATRIX16:def 7
it is_line_circulant_about p;

existence
ex b₁ being Matrix of len p,K st b₁ is_line_circulant_about p by A1;
uniqueness
for b₁, b₂ being Matrix of len p,K st b₁ is_line_circulant_about p & b₂ is_line_circulant_about p holds
b₁ = b₂

proof end;

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₃ being Matrix of len p,K holds
( b₃ = LCirc p iff b₃ is_line_circulant_about p );

definition

let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-col-of-circulant ;

func CCirc p -> Matrix of len p,K means :Def8: :: MATRIX16:def 8
it is_col_circulant_about p;

existence
ex b₁ being Matrix of len p,K st b₁ is_col_circulant_about p by A1;
uniqueness
for b₁, b₂ being Matrix of len p,K st b₁ is_col_circulant_about p & b₂ is_col_circulant_about p holds
b₁ = b₂

proof end;

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₃ being Matrix of len p,K holds
( b₃ = CCirc p iff b₃ is_col_circulant_about p );

registration

let K be Field;

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₁ being FinSequence of K st
( b₁ is first-line-of-circulant & b₁ is first-col-of-circulant )

proof end;

end;

registration

let K be Field;
let n be Element of NAT ;

cluster 0. (K,n) -> line_circulant col_circulant ;

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

proof end;

end;

registration

let K be Field;
let n be Element of NAT ;
let a be Element of K;

cluster (n,n) --> a -> line_circulant for Matrix of n,K;

coherence
for b₁ being Matrix of n,K st b₁ = (n,n) --> a holds
b₁ is line_circulant

proof end;

cluster (n,n) --> a -> col_circulant for Matrix of n,K;

coherence
for b₁ being Matrix of n,K st b₁ = (n,n) --> a holds
b₁ is col_circulant

proof end;

end;

registration

let K be Field;

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₁ being Matrix of K st
( b₁ is line_circulant & b₁ is col_circulant )

proof end;

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

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)

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)

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

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

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

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

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

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

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

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

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

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

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

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

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)

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)

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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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)

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

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)

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

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)

proof end;

theorem :: MATRIX16:39

for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is col_circulant

proof end;

theorem :: MATRIX16:40

for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is line_circulant

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

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)

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)

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))

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))

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

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)

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)

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))

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))

proof end;

notation

let K be set ;
let M be Matrix of K;
synonym circulant M for line_circulant ;

end;

definition

let K be Field;
let M1 be Matrix of K;
let p be FinSequence of K;

pred M1 is_anti-circular_about p means :: MATRIX16:def 9
( 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) ) );

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) ) ) );

definition

let K be Field;
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 );

end;

:: 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 ) );

definition

let K be Field;
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;

end;

:: 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 );

definition

let K be Field;
let p be FinSequence of K;
assume A1: p is first-line-of-anti-circular ;

func ACirc p -> Matrix of len p,K means :Def12: :: MATRIX16:def 12
it is_anti-circular_about p;

existence
ex b₁ being Matrix of len p,K st b₁ is_anti-circular_about p by A1;
uniqueness
for b₁, b₂ being Matrix of len p,K st b₁ is_anti-circular_about p & b₂ is_anti-circular_about p holds
b₁ = b₂

proof end;

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₃ being Matrix of len p,K holds
( b₃ = ACirc p iff b₃ is_anti-circular_about p );

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

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

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

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)

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

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

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)

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

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)

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

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)

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

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)

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)

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))

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))

proof end;

registration

let K be Field;
let n be Element of NAT ;

cluster 0. (K,n) -> anti-circular ;

coherence
0. (K,n) is anti-circular

proof end;

end;