theorem :: MATRIX16:39

for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is col_circulant