theorem Th31: :: MATRIX16:31

for K being Field
for p being FinSequence of K st p is first-line-of-circulant holds
- p is first-line-of-circulant