:: Basic Properties of Circulant Matrices and Anti-circular Matrices
:: by Xiaopeng Yue and Xiquan Liang
::
:: Received August 26, 2008
:: Copyright (c) 2008 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
Lm2a:
for n, i, j being Nat st i in Seg n & j in Seg n holds
((j - i) mod n) + 1 in Seg n
Lm2:
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
theorem :: MATRIX16:1
theorem :: MATRIX16:2
:: deftheorem Def1 defines is_line_circulant_about MATRIX16:def 1 :
:: deftheorem Def2 defines line_circulant MATRIX16:def 2 :
:: deftheorem Def3 defines first-line-of-circulant MATRIX16:def 3 :
:: deftheorem Def4 defines is_col_circulant_about MATRIX16:def 4 :
:: deftheorem Def5 defines col_circulant MATRIX16:def 5 :
:: deftheorem Def6 defines first-col-of-circulant MATRIX16:def 6 :
:: deftheorem Def7 defines LCirc MATRIX16:def 7 :
:: deftheorem Def8 defines CCirc MATRIX16:def 8 :
theorem :: MATRIX16:3
theorem :: MATRIX16:4
theorem :: MATRIX16:5
theorem Th6: :: MATRIX16:6
theorem Th7: :: MATRIX16:7
theorem Th8: :: MATRIX16:8
theorem :: MATRIX16:9
theorem :: MATRIX16:10
theorem Th11: :: MATRIX16:11
theorem :: MATRIX16:12
theorem Th13: :: MATRIX16:13
theorem :: MATRIX16:14
theorem :: MATRIX16:15
theorem :: MATRIX16:16
theorem :: MATRIX16:17
theorem :: MATRIX16:18
theorem :: MATRIX16:19
theorem Th20: :: MATRIX16:20
theorem Th21: :: MATRIX16:21
theorem Th22: :: MATRIX16:22
theorem :: MATRIX16:23
theorem :: MATRIX16:24
theorem Th25: :: MATRIX16:25
theorem :: MATRIX16:26
theorem Th27: :: MATRIX16:27
theorem :: MATRIX16:28
theorem :: MATRIX16:29
theorem :: MATRIX16:30
theorem Th31: :: MATRIX16:31
theorem :: MATRIX16:32
theorem Th33: :: MATRIX16:33
theorem Th34: :: MATRIX16:34
theorem Th35: :: MATRIX16:35
theorem :: MATRIX16:36
theorem Th37: :: MATRIX16:37
theorem Th38: :: MATRIX16:38
theorem :: MATRIX16:39
theorem :: MATRIX16:40
theorem Th41: :: MATRIX16:41
theorem Th42: :: MATRIX16:42
theorem :: MATRIX16:43
theorem :: MATRIX16:44
theorem :: MATRIX16:45
theorem Th46: :: MATRIX16:46
theorem Th47: :: MATRIX16:47
theorem :: MATRIX16:48
theorem :: MATRIX16:49
theorem :: MATRIX16:50
:: deftheorem Def10 defines is_anti-circular_about MATRIX16:def 9 :
:: deftheorem Def11 defines anti-circular MATRIX16:def 10 :
:: deftheorem Def12 defines first-line-of-anti-circular MATRIX16:def 11 :
:: deftheorem Def13 defines ACirc MATRIX16:def 12 :
theorem :: MATRIX16:51
theorem Th52: :: MATRIX16:52
theorem :: MATRIX16:53
theorem :: MATRIX16:54
theorem Th55: :: MATRIX16:55
theorem :: MATRIX16:56
theorem :: MATRIX16:57
theorem Th58: :: MATRIX16:58
theorem :: MATRIX16:59
theorem Th60: :: MATRIX16:60
theorem Th61: :: MATRIX16:61
theorem Th62: :: MATRIX16:62
theorem Th63: :: MATRIX16:63
theorem :: MATRIX16:64
theorem :: MATRIX16:65
theorem :: MATRIX16:66