theorem Th17: :: MATRIX17:17
for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is symmetry_circulant holds
M1 @ = M1