begin
definition
let M be
Matrix of
COMPLEX ;
func M *' -> Matrix of
COMPLEX means :
Def1:
(
len it = len M &
width it = width M & ( for
i,
j being
Nat st
[i,j] in Indices M holds
it * i,
j = (M * i,j) *' ) );
existence
ex b1 being Matrix of COMPLEX st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = (M * i,j) *' ) )
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = (M * i,j) *' ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * i,j = (M * i,j) *' ) holds
b1 = b2
end;
:: deftheorem Def1 defines *' MATRIXC1:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem Th13:
theorem Th14:
theorem
:: deftheorem defines @" MATRIXC1:def 2 :
:: deftheorem defines FinSeq2Matrix MATRIXC1:def 3 :
:: deftheorem defines Matrix2FinSeq MATRIXC1:def 4 :
:: deftheorem defines mlt MATRIXC1:def 5 :
:: deftheorem MATRIXC1:def 6 :
canceled;
:: deftheorem Def7 defines * MATRIXC1:def 7 :
Lm1:
for a being Element of COMPLEX
for F being FinSequence of COMPLEX holds a * F = (multcomplex [;] a,(id COMPLEX )) * F
theorem Th16:
:: deftheorem defines * MATRIXC1:def 8 :
theorem
theorem
canceled;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
Lm2:
for a, b being Element of COMPLEX holds (multcomplex [;] a,(id COMPLEX )) . b = a * b
theorem Th29:
:: deftheorem defines FR2FC MATRIXC1:def 9 :
theorem
theorem
theorem Th32:
theorem
theorem Th34:
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem
canceled;
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem
theorem
theorem
canceled;
theorem Th49:
:: deftheorem Def10 defines LineSum MATRIXC1:def 10 :
:: deftheorem Def11 defines ColSum MATRIXC1:def 11 :
theorem Th50:
theorem Th51:
theorem Th52:
:: deftheorem defines SumAll MATRIXC1:def 12 :
theorem Th53:
theorem Th54:
definition
let x,
y be
FinSequence of
COMPLEX ;
let M be
Matrix of
COMPLEX ;
assume that A1:
len x = len M
and A2:
len y = width M
;
func QuadraticForm x,
M,
y -> Matrix of
COMPLEX means :
Def13:
(
len it = len x &
width it = len y & ( for
i,
j being
Nat st
[i,j] in Indices M holds
it * i,
j = ((x . i) * (M * i,j)) * ((y . j) *' ) ) );
existence
ex b1 being Matrix of COMPLEX st
( len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = ((x . i) * (M * i,j)) * ((y . j) *' ) ) )
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = ((x . i) * (M * i,j)) * ((y . j) *' ) ) & len b2 = len x & width b2 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b2 * i,j = ((x . i) * (M * i,j)) * ((y . j) *' ) ) holds
b1 = b2
end;
:: deftheorem Def13 defines QuadraticForm MATRIXC1:def 13 :
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem