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