:: Basic Properties of Circulant Matrices and Anti-circular Matrices
:: by Xiaopeng Yue and Xiquan Liang
::
:: Received August 26, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

Lm1:  for n being Element of NAT
for k being Nat st k <= n &amp; k >= 1 holds
(k - 1) mod n = k - 1
proofend;

Lm2:  for n, i, j being Nat st i in Seg n &amp; j in Seg n holds
((j - i) mod n) + 1 in Seg n
proofend;

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

theorem :: MATRIX16:1
for K being Field
for p being FinSequence of K holds (1_ K) * p = p
proofend;

theorem :: MATRIX16:2
for K being Field
for p being FinSequence of K holds (- (1_ K)) * p = - p
proofend;

definition
let K be set ;
let M be Matrix of K;
let p be FinSequence;
predM is_line_circulant_about p means :Def1: :: MATRIX16:def 1
( len p = width M &amp; ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((j - i) mod (len p)) + 1) ) );
end;

:: deftheorem Def1 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 &amp; ( 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;
attrM is line_circulant  means :Def2: :: MATRIX16:def 2
 ex p being FinSequence of K st
( len p = width M &amp; M is_line_circulant_about p );
end;

:: deftheorem Def2 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 &amp; M is_line_circulant_about p ) );

definition
let K be non empty set ;
let p be FinSequence of K;
attrp is first-line-of-circulant  means :Def3: :: MATRIX16:def 3
 ex M being Matrix of len p,K st M is_line_circulant_about p;
end;

:: deftheorem Def3 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;
predM is_col_circulant_about p means :Def4: :: MATRIX16:def 4
( len p = len M &amp; ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((i - j) mod (len p)) + 1) ) );
end;

:: deftheorem Def4 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 &amp; ( 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;
attrM is col_circulant  means :Def5: :: MATRIX16:def 5
 ex p being FinSequence of K st
( len p = len M &amp; M is_col_circulant_about p );
end;

:: deftheorem Def5 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 &amp; M is_col_circulant_about p ) );

definition
let K be non empty set ;
let p be FinSequence of K;
attrp is first-col-of-circulant  means :Def6: :: MATRIX16:def 6
 ex M being Matrix of len p,K st M is_col_circulant_about p;
end;

:: deftheorem Def6 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 b1 being Matrix of len p,K st b1 is_line_circulant_about p by A1, Def3;
uniqueness
 for b1, b2 being Matrix of len p,K st b1 is_line_circulant_about p &amp; b2 is_line_circulant_about p holds
b1 = b2
proofend;
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 b3 being Matrix of len p,K holds
( b3 = LCirc p iff b3 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 b1 being Matrix of len p,K st b1 is_col_circulant_about p by A1, Def6;
uniqueness
 for b1, b2 being Matrix of len p,K st b1 is_col_circulant_about p &amp; b2 is_col_circulant_about p holds
b1 = b2
proofend;
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 b3 being Matrix of len p,K holds
( b3 = CCirc p iff b3 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 b1 being FinSequence of K st
( b1 is first-line-of-circulant &amp; b1 is first-col-of-circulant )
proofend;
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 &amp; 0. (K,n) is col_circulant )
proofend;
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 b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is line_circulant
proofend;
cluster(n,n) --> a ->  col_circulant for Matrix of n,K;
coherence
 for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is col_circulant
proofend;
end;

registration
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular line_circulant col_circulant for FinSequence of the carrier of K * ;
existence
 ex b1 being Matrix of K st
( b1 is line_circulant &amp; b1 is col_circulant )
proofend;
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 &amp; n > 0 holds
A @ is col_circulant
proofend;

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 &amp; n > 0 holds
t = Line (A,1)
proofend;

theorem :: MATRIX16:5
for i, j, n, k, l being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is line_circulant &amp; [i,j] in [:(Seg n),(Seg n):] &amp; k = i + 1 &amp; l = j + 1 &amp; i < n &amp; j < n holds
A * (i,j) = A * (k,l)
proofend;

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

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 &amp; M2 is line_circulant holds
M1 + M2 is line_circulant
proofend;

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 &amp; M2 is line_circulant &amp; M3 is line_circulant holds
(M1 + M2) + M3 is line_circulant
proofend;

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 &amp; M2 is line_circulant holds
(a * M1) + (b * M2) is line_circulant
proofend;

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 &amp; M2 is line_circulant &amp; M3 is line_circulant holds
((a * M1) + (b * M2)) + (c * M3) is line_circulant
proofend;

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

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 &amp; M2 is line_circulant holds
M1 - M2 is line_circulant
proofend;

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 &amp; M2 is line_circulant holds
(a * M1) - (b * M2) is line_circulant
proofend;

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 &amp; M2 is line_circulant &amp; M3 is line_circulant holds
((a * M1) + (b * M2)) - (c * M3) is line_circulant
proofend;

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 &amp; M2 is line_circulant &amp; M3 is line_circulant holds
((a * M1) - (b * M2)) - (c * M3) is line_circulant
proofend;

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 &amp; M2 is line_circulant &amp; M3 is line_circulant holds
((a * M1) - (b * M2)) + (c * M3) is line_circulant
proofend;

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 &amp; n > 0 holds
A @ is line_circulant
proofend;

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 &amp; n > 0 holds
t = Col (A,1)
proofend;

theorem :: MATRIX16:19
for i, j, n, k, l being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is col_circulant &amp; [i,j] in [:(Seg n),(Seg n):] &amp; k = i + 1 &amp; l = j + 1 &amp; i < n &amp; j < n holds
A * (i,j) = A * (k,l)
proofend;

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

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 &amp; M2 is col_circulant holds
M1 + M2 is col_circulant
proofend;

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 &amp; M2 is col_circulant &amp; M3 is col_circulant holds
(M1 + M2) + M3 is col_circulant
proofend;

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 &amp; M2 is col_circulant holds
(a * M1) + (b * M2) is col_circulant
proofend;

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 &amp; M2 is col_circulant &amp; M3 is col_circulant holds
((a * M1) + (b * M2)) + (c * M3) is col_circulant
proofend;

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

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 &amp; M2 is col_circulant holds
M1 - M2 is col_circulant
proofend;

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 &amp; M2 is col_circulant holds
(a * M1) - (b * M2) is col_circulant
proofend;

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 &amp; M2 is col_circulant &amp; M3 is col_circulant holds
((a * M1) + (b * M2)) - (c * M3) is col_circulant
proofend;

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 &amp; M2 is col_circulant &amp; M3 is col_circulant holds
((a * M1) - (b * M2)) - (c * M3) is col_circulant
proofend;

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 &amp; M2 is col_circulant &amp; M3 is col_circulant holds
((a * M1) - (b * M2)) + (c * M3) is col_circulant
proofend;

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

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

theorem Th33: :: MATRIX16:33
for K being Field
for p, q being FinSequence of K st p is first-line-of-circulant &amp; q is first-line-of-circulant &amp; len p = len q holds
p + q is first-line-of-circulant
proofend;

theorem Th34: :: MATRIX16:34
for K being Field
for p, q being FinSequence of K st len p = len q &amp; p is first-line-of-circulant &amp; q is first-line-of-circulant holds
LCirc (p + q) = (LCirc p) + (LCirc q)
proofend;

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

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

theorem Th37: :: MATRIX16:37
for K being Field
for p, q being FinSequence of K st p is first-col-of-circulant &amp; q is first-col-of-circulant &amp; len p = len q holds
p + q is first-col-of-circulant
proofend;

theorem Th38: :: MATRIX16:38
for K being Field
for p, q being FinSequence of K st len p = len q &amp; p is first-col-of-circulant &amp; q is first-col-of-circulant holds
CCirc (p + q) = (CCirc p) + (CCirc q)
proofend;

theorem :: MATRIX16:39
for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is col_circulant
proofend;

theorem :: MATRIX16:40
for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is line_circulant
proofend;

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

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

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

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 &amp; q is first-line-of-circulant &amp; len p = len q holds
(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
proofend;

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 &amp; q is first-line-of-circulant &amp; len p = len q holds
(a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q))
proofend;

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

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

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

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 &amp; q is first-col-of-circulant &amp; len p = len q &amp; len p > 0 holds
(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))
proofend;

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 &amp; q is first-col-of-circulant &amp; len p = len q holds
(a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))
proofend;

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

begin

definition
let K be Field;
let M1 be Matrix of K;
let p be FinSequence of K;
predM1 is_anti-circular_about p means :Def9: :: MATRIX16:def 9
( len p = width M1 &amp; ( for i, j being Nat st [i,j] in Indices M1 &amp; i <= j holds
M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) &amp; ( for i, j being Nat st [i,j] in Indices M1 &amp; i >= j holds
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) );
end;

:: deftheorem Def9 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 &amp; ( for i, j being Nat st [i,j] in Indices M1 &amp; i <= j holds
M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) &amp; ( for i, j being Nat st [i,j] in Indices M1 &amp; i >= j holds
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) ) );

definition
let K be Field;
let M be Matrix of K;
attrM is anti-circular  means :Def10: :: MATRIX16:def 10
 ex p being FinSequence of K st
( len p = width M &amp; M is_anti-circular_about p );
end;

:: deftheorem Def10 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 &amp; M is_anti-circular_about p ) );

definition
let K be Field;
let p be FinSequence of K;
attrp is first-line-of-anti-circular  means :Def11: :: MATRIX16:def 11
 ex M being Matrix of len p,K st M is_anti-circular_about p;
end;

:: deftheorem Def11 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 b1 being Matrix of len p,K st b1 is_anti-circular_about p by A1, Def11;
uniqueness
 for b1, b2 being Matrix of len p,K st b1 is_anti-circular_about p &amp; b2 is_anti-circular_about p holds
b1 = b2
proofend;
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 b3 being Matrix of len p,K holds
( b3 = ACirc p iff b3 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
proofend;

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 &amp; M2 is anti-circular holds
M1 + M2 is anti-circular
proofend;

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 &amp; i = j &amp; M1 is anti-circular holds
M1 * (i,j) = 0. K
proofend;

theorem :: MATRIX16:54
for i, j, n, k, l being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is anti-circular &amp; [i,j] in [:(Seg n),(Seg n):] &amp; k = i + 1 &amp; l = j + 1 &amp; i < n &amp; j < n holds
M1 * (k,l) = M1 * (i,j)
proofend;

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

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 &amp; M2 is anti-circular holds
M1 - M2 is anti-circular
proofend;

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 &amp; n > 0 holds
p = Line (M1,1)
proofend;

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

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

theorem Th60: :: MATRIX16:60
for K being Field
for p, q being FinSequence of K st p is first-line-of-anti-circular &amp; q is first-line-of-anti-circular &amp; len p = len q holds
p + q is first-line-of-anti-circular
proofend;

theorem Th61: :: MATRIX16:61
for K being Field
for p, q being FinSequence of K st p is first-line-of-anti-circular &amp; q is first-line-of-anti-circular &amp; len p = len q holds
ACirc (p + q) = (ACirc p) + (ACirc q)
proofend;

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

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

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

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 &amp; q is first-line-of-anti-circular &amp; len p = len q holds
(a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))
proofend;

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 &amp; q is first-line-of-anti-circular &amp; len p = len q holds
(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
proofend;

registration
let K be Field;
let n be Element of NAT ;
cluster 0. (K,n) ->  anti-circular ;
coherence
 0. (K,n) is anti-circular
proofend;
end;