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