:: deftheorem defines anti-circular MATRIX16:def 10 :
for K being Field
for M being Matrix of K holds
( M is anti-circular iff ex p being FinSequence of K st
( len p = width M & M is_anti-circular_about p ) );