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