let n be Element of NAT ; for K being Field st n > 0 holds
1. (K,n) is col_circulant
let K be Field; ( n > 0 implies 1. (K,n) is col_circulant )
assume A1:
n > 0
; 1. (K,n) is col_circulant
set M1 = 1. (K,n);
A2:
Indices (1. (K,n)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
set p = Col ((1. (K,n)),1);
A3:
len (1. (K,n)) = n
by MATRIX_0:24;
then A4:
len (Col ((1. (K,n)),1)) = n
by MATRIX_0:def 8;
A5:
dom (1. (K,n)) = Seg n
by A3, FINSEQ_1:def 3;
A6:
width (1. (K,n)) = n
by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) )
A7:
(i - j) mod n >= 0
by A1, NAT_D:62;
then A8:
((i - j) mod n) + 1
in NAT
by INT_1:3;
assume A9:
[i,j] in Indices (1. (K,n))
;
(1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
then A10:
j in Seg n
by A2, ZFMISC_1:87;
then A11:
1
<= j
by FINSEQ_1:1;
A12:
j <= n
by A10, FINSEQ_1:1;
A13:
i in Seg n
by A2, A9, ZFMISC_1:87;
then
1
<= i
by FINSEQ_1:1;
then A14:
1
- n <= i - j
by A12, XREAL_1:13;
- n <= (- n) + 1
by XREAL_1:29;
then A15:
- n <= i - j
by A14, XXREAL_0:2;
i <= n
by A13, FINSEQ_1:1;
then A16:
i - j <= n - 1
by A11, XREAL_1:13;
n - 1
< n
by XREAL_1:44;
then A17:
i - j < n
by A16, XXREAL_0:2;
(i - j) mod n <= n - 1
then A19:
((i - j) mod n) + 1
<= (n - 1) + 1
by XREAL_1:6;
((i - j) mod n) + 1
>= 0 + 1
by A7, XREAL_1:6;
then A20:
((i - j) mod n) + 1
in Seg n
by A19, A8;
then A21:
((i - j) mod (len (Col ((1. (K,n)),1)))) + 1
in Seg n
by A3, MATRIX_0:def 8;
(1. (K,n)) * (
i,
j)
= (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
proof
per cases
( i = j or i <> j )
;
suppose A22:
i = j
;
(1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
0 + 1
<= n
by A1, NAT_1:13;
then
1
in Seg n
;
then A23:
[1,1] in Indices (1. (K,n))
by A2, ZFMISC_1:87;
(i - j) mod (len (Col ((1. (K,n)),1))) = 0
by A1, A4, A22, NAT_D:63;
then (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1) =
(1. (K,n)) * (1,1)
by A5, A21, MATRIX_0:def 8
.=
1_ K
by A23, MATRIX_1:def 3
;
hence
(1. (K,n)) * (
i,
j)
= (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
by A9, A22, MATRIX_1:def 3;
verum end; suppose A24:
i <> j
;
(1. (K,n)) * (i,j) = (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)then A25:
i - j <> 0
;
(i - j) mod n <> 0
then A27:
((i - j) mod (len (Col ((1. (K,n)),1)))) + 1
<> 1
by A3, MATRIX_0:def 8;
set l =
((i - j) mod (len (Col ((1. (K,n)),1)))) + 1;
reconsider l =
((i - j) mod (len (Col ((1. (K,n)),1)))) + 1 as
Nat by A3, A8, MATRIX_0:def 8;
0 + 1
<= n
by A1, NAT_1:13;
then A28:
1
in Seg n
;
l in dom (1. (K,n))
by A3, A4, A20, FINSEQ_1:def 3;
then A29:
[l,1] in Indices (1. (K,n))
by A6, A28, ZFMISC_1:87;
(Col ((1. (K,n)),1)) . l =
(1. (K,n)) * (
l,1)
by A5, A21, MATRIX_0:def 8
.=
0. K
by A27, A29, MATRIX_1:def 3
;
hence
(1. (K,n)) * (
i,
j)
= (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
by A9, A24, MATRIX_1:def 3;
verum end;
end;
hence
(1. (K,n)) * (
i,
j)
= (Col ((1. (K,n)),1)) . (((i - j) mod (len (Col ((1. (K,n)),1)))) + 1)
;
verum
end;
then
1. (K,n) is_col_circulant_about Col ((1. (K,n)),1)
by A3, A4;
then consider p being FinSequence of K such that
A30:
( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p )
;
take
p
; MATRIX16:def 5 ( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p )
thus
( len p = len (1. (K,n)) & 1. (K,n) is_col_circulant_about p )
by A30; verum