theorem Th13: :: MATRIX17:13

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