:: deftheorem defines first-col-of-circulant MATRIX16:def 6 :
for K being non empty set
for p being FinSequence of K holds
( p is first-col-of-circulant iff ex M being Matrix of len p,K st M is_col_circulant_about p );