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
A2: 0 < n and
A4: A is_symmetry_circulant_about p ; :: thesis: A @ is_symmetry_circulant_about p
A3: len p = width A by A4, Def4;
( width A = n & len A = n ) by MATRIX_1:24;
then A5: width (A @) = len p by A2, A3, MATRIX_2:10;
A6: 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)) )
A7: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume that
A8: [i,j] in Indices (A @) and
A9: i + j <> (len p) + 1 ; :: thesis: (A @) * (i,j) = p . (((i + j) - 1) mod (len p))
[i,j] in Indices A by A8, MATRIX_1:26;
then ( i in Seg n & j in Seg n ) by A7, ZFMISC_1:87;
then A10: [j,i] in Indices A by A7, ZFMISC_1:87;
then (A @) * (i,j) = A * (j,i) by MATRIX_1:def 6;
hence (A @) * (i,j) = p . (((i + j) - 1) mod (len p)) by A4, A10, A9, Def4; :: 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) )
A11: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume that
A12: [i,j] in Indices (A @) and
A13: i + j = (len p) + 1 ; :: thesis: (A @) * (i,j) = p . (len p)
[i,j] in Indices A by A12, MATRIX_1:26;
then ( i in Seg n & j in Seg n ) by A11, ZFMISC_1:87;
then A14: [j,i] in Indices A by A11, ZFMISC_1:87;
then (A @) * (i,j) = A * (j,i) by MATRIX_1:def 6;
hence (A @) * (i,j) = p . (len p) by A4, A13, A14, Def4; :: thesis: verum

end;

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