let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( [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 ; :: thesis: (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; :: thesis: 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; :: thesis: ( [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 ; :: thesis: (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; :: thesis: verum

end;

hence A @ is_symmetry_circulant_about p by A4, A5; :: thesis: verum