let n be Element of NAT ; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is col_circulant holds
- M1 is col_circulant
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is col_circulant holds
- M1 is col_circulant
let M1 be Matrix of n,K; :: thesis: ( M1 is col_circulant implies - M1 is col_circulant )
assume A1: M1 is col_circulant ; :: thesis: - M1 is col_circulant
consider p being FinSequence of K such that
A2: ( len p = len M1 & M1 is_col_circulant_about p ) by A1, Def5;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = n & width M1 = n & Indices (- M1) = [:(Seg n),(Seg n):] & len (- M1) = n & width (- M1) = n ) by MATRIX_1:25;
then A5: ( len p = n & dom p = Seg n ) by A2, FINSEQ_1:def 3;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
then A6: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:133;
then A7: len (- p) = len p by FINSEQ_1:def 18;
for i, j being Nat st [i,j] in Indices (- M1) holds
(- M1) * i,j = (- p) . (((i - j) mod (len (- p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (- M1) implies (- M1) * i,j = (- p) . (((i - j) mod (len (- p))) + 1) )
assume B1: [i,j] in Indices (- M1) ; :: thesis: (- M1) * i,j = (- p) . (((i - j) mod (len (- p))) + 1)
then B3: ((i - j) mod n) + 1 in Seg n by A4, Lm2;
(- M1) * i,j = - (M1 * i,j) by B1, A4, MATRIX_3:def 2
.= (comp K) . (M1 * i,j) by VECTSP_1:def 25
.= (comp K) . (p . (((i - j) mod (len p)) + 1)) by B1, A4, A2, Def4
.= (- p) . (((i - j) mod (len p)) + 1) by B3, A5, FUNCT_1:23 ;
hence (- M1) * i,j = (- p) . (((i - j) mod (len (- p))) + 1) by A6, FINSEQ_1:def 18; :: thesis: verum

end;

then A9: - M1 is_col_circulant_about - p by A7, A2, A4, Def4;
set r = - p;
consider r being FinSequence of K such that
A10: ( len r = len (- M1) & - M1 is_col_circulant_about r ) by A7, A2, A4, A9;
take r ; :: according to MATRIX16:def 5 :: thesis: ( len r = len (- M1) & - M1 is_col_circulant_about r )
thus ( len r = len (- M1) & - M1 is_col_circulant_about r ) by A10; :: thesis: verum