theorem :: MATRIX16:17

for n being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is col_circulant & n > 0 holds
A @ is line_circulant