:: deftheorem defines is_anti-circular_about MATRIX16:def 9 :
for K being Field
for M1 being Matrix of K
for p being FinSequence of K holds
( M1 is_anti-circular_about p iff ( len p = width M1 & ( for i, j being Nat st [i,j] in Indices M1 & i <= j holds
M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) & ( for i, j being Nat st [i,j] in Indices M1 & i >= j holds
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) ) );