:: deftheorem defines is_symmetry_circulant_about MATRIX17:def 4 :
for K being set
for M being Matrix of K
for p being FinSequence holds
( M is_symmetry_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M & i + j <> (len p) + 1 holds
M * (i,j) = p . (((i + j) - 1) mod (len p)) ) & ( for i, j being Nat st [i,j] in Indices M & i + j = (len p) + 1 holds
M * (i,j) = p . (len p) ) ) );