theorem :: MATRIX16:32
for K being Field
for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (- p) = - (LCirc p)