theorem Th42: :: MATRIX16:42

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