let n be Nat; for D being non empty set
for A being Matrix of n,D
for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
let D be non empty set ; for A being Matrix of n,D
for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
let A be Matrix of n,D; for p being FinSequence of D st 0 < n & A is_symmetry_circulant_about p holds
A @ is_symmetry_circulant_about p
let p be FinSequence of D; ( 0 < n & A is_symmetry_circulant_about p implies A @ is_symmetry_circulant_about p )
assume that
A1:
0 < n
and
A2:
A is_symmetry_circulant_about p
; A @ is_symmetry_circulant_about p
A3:
len p = width A
by A2;
( width A = n & len A = n )
by MATRIX_0:24;
then A4:
width (A @) = len p
by A1, A3, MATRIX_0:54;
A5:
for i, j being Nat st [i,j] in Indices (A @) & i + j <> (len p) + 1 holds
(A @) * (i,j) = p . (((i + j) - 1) mod (len p))
proof
let i,
j be
Nat;
( [i,j] in Indices (A @) & i + j <> (len p) + 1 implies (A @) * (i,j) = p . (((i + j) - 1) mod (len p)) )
A6:
Indices A = [:(Seg n),(Seg n):]
by MATRIX_0:24;
assume that A7:
[i,j] in Indices (A @)
and A8:
i + j <> (len p) + 1
;
(A @) * (i,j) = p . (((i + j) - 1) mod (len p))
[i,j] in Indices A
by A7, MATRIX_0:26;
then
(
i in Seg n &
j in Seg n )
by A6, ZFMISC_1:87;
then A9:
[j,i] in Indices A
by A6, ZFMISC_1:87;
then
(A @) * (
i,
j)
= A * (
j,
i)
by MATRIX_0:def 6;
hence
(A @) * (
i,
j)
= p . (((i + j) - 1) mod (len p))
by A2, A9, A8;
verum
end;
for i, j being Nat st [i,j] in Indices (A @) & i + j = (len p) + 1 holds
(A @) * (i,j) = p . (len p)
proof
let i,
j be
Nat;
( [i,j] in Indices (A @) & i + j = (len p) + 1 implies (A @) * (i,j) = p . (len p) )
A10:
Indices A = [:(Seg n),(Seg n):]
by MATRIX_0:24;
assume that A11:
[i,j] in Indices (A @)
and A12:
i + j = (len p) + 1
;
(A @) * (i,j) = p . (len p)
[i,j] in Indices A
by A11, MATRIX_0:26;
then
(
i in Seg n &
j in Seg n )
by A10, ZFMISC_1:87;
then A13:
[j,i] in Indices A
by A10, ZFMISC_1:87;
then
(A @) * (
i,
j)
= A * (
j,
i)
by MATRIX_0:def 6;
hence
(A @) * (
i,
j)
= p . (len p)
by A2, A12, A13;
verum
end;
hence
A @ is_symmetry_circulant_about p
by A4, A5; verum