let n be Element of NAT ; for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let K be Field; for a being Element of K
for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let a be Element of K; for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
let M1 be Matrix of n,K; ( M1 is col_circulant implies a * M1 is col_circulant )
A1:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
assume
M1 is col_circulant
; a * M1 is col_circulant
then consider p being FinSequence of K such that
A2:
len p = len M1
and
A3:
M1 is_col_circulant_about p
;
A4:
len M1 = n
by MATRIX_0:24;
then A5:
dom p = Seg n
by A2, FINSEQ_1:def 3;
A6:
len (a * p) = len p
by MATRIXR1:16;
A7:
dom (a * p) = Seg (len (a * p))
by FINSEQ_1:def 3;
A8:
for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) = (a * p) . (((i - j) mod (len p)) + 1)
proof
let i,
j be
Nat;
( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) = (a * p) . (((i - j) mod (len p)) + 1) )
assume
[i,j] in Indices (a * M1)
;
(a * M1) * (i,j) = (a * p) . (((i - j) mod (len p)) + 1)
then A9:
[i,j] in Indices M1
by MATRIX_0:26;
then A10:
((i - j) mod (len p)) + 1
in Seg n
by A2, A1, A4, Lm3;
(a * M1) * (
i,
j) =
a * (M1 * (i,j))
by A9, MATRIX_3:def 5
.=
(a multfield) . (M1 * (i,j))
by FVSUM_1:49
.=
(a multfield) . (p . (((i - j) mod (len p)) + 1))
by A3, A9
.=
(a multfield) . (p /. (((i - j) mod (len p)) + 1))
by A5, A10, PARTFUN1:def 6
.=
a * (p /. (((i - j) mod (len p)) + 1))
by FVSUM_1:49
.=
(a * p) /. (((i - j) mod (len p)) + 1)
by A5, A10, POLYNOM1:def 1
.=
(a * p) . (((i - j) mod (len p)) + 1)
by A2, A4, A6, A7, A10, PARTFUN1:def 6
;
hence
(a * M1) * (
i,
j)
= (a * p) . (((i - j) mod (len p)) + 1)
;
verum
end;
A11:
len (a * M1) = n
by MATRIX_0:24;
len p = n
by A2, MATRIX_0:24;
then
a * M1 is_col_circulant_about a * p
by A11, A6, A8;
then consider q being FinSequence of K such that
A12:
( len q = len (a * M1) & a * M1 is_col_circulant_about q )
;
take
q
; MATRIX16:def 5 ( len q = len (a * M1) & a * M1 is_col_circulant_about q )
thus
( len q = len (a * M1) & a * M1 is_col_circulant_about q )
by A12; verum