theorem Th47: :: MATRIX16:47
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (a * p) = a * (CCirc p)