:: deftheorem defines col_circulant MATRIX16:def 5 :
for K being set
for M being Matrix of K holds
( M is col_circulant iff ex p being FinSequence of K st
( len p = len M & M is_col_circulant_about p ) );