begin
Lm1:
for n being Element of NAT
for k being Nat st k <= n & k >= 1 holds
(k - 1) mod n = k - 1
Lm2:
for n, i, j being Nat st i in Seg n & j in Seg n holds
((j - i) mod n) + 1 in Seg n
Lm3:
for n, i, j being Nat st ( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] ) holds
((j - i) mod n) + 1 in Seg n
theorem
theorem
:: deftheorem Def1 defines is_line_circulant_about MATRIX16:def 1 :
:: deftheorem Def2 defines line_circulant MATRIX16:def 2 :
:: deftheorem Def3 defines first-line-of-circulant MATRIX16:def 3 :
:: deftheorem Def4 defines is_col_circulant_about MATRIX16:def 4 :
:: deftheorem Def5 defines col_circulant MATRIX16:def 5 :
:: deftheorem Def6 defines first-col-of-circulant MATRIX16:def 6 :
:: deftheorem Def7 defines LCirc MATRIX16:def 7 :
:: deftheorem Def8 defines CCirc MATRIX16:def 8 :
theorem
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem
theorem Th11:
theorem
theorem Th13:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem
theorem Th25:
theorem
theorem Th27:
theorem
theorem
theorem
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem
theorem
theorem Th41:
theorem Th42:
theorem
theorem
theorem
theorem Th46:
theorem Th47:
theorem
theorem
theorem
begin
:: deftheorem Def9 defines is_anti-circular_about MATRIX16:def 9 :
:: deftheorem Def10 defines anti-circular MATRIX16:def 10 :
:: deftheorem Def11 defines first-line-of-anti-circular MATRIX16:def 11 :
:: deftheorem Def12 defines ACirc MATRIX16:def 12 :
theorem
theorem Th52:
theorem
theorem
theorem Th55:
theorem
theorem
theorem Th58:
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem
theorem
theorem