theorem Th12: :: MATRIX17:12

for K being Field
for a being Element of K
for p being FinSequence of K st p is first-symmetry-of-circulant holds
a * p is first-symmetry-of-circulant