begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
for
n,
i,
j being
Nat st
i in Seg (n + 1) &
n >= 2 holds
ex
Proj being
Function of
2Set (Seg n),
2Set (Seg (n + 1)) st
(
rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 1)) } &
Proj is
one-to-one & ( for
k,
m being
Nat st
k < m &
{k,m} in 2Set (Seg n) holds
( (
m < i &
k < i implies
Proj . {k,m} = {k,m} ) & (
m >= i &
k < i implies
Proj . {k,m} = {k,(m + 1)} ) & (
m >= i &
k >= i implies
Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )
theorem Th11:
theorem Th12:
for
X,
Y,
D being non
empty set for
f being
Function of
X,
Fin Y for
g being
Function of
Fin Y,
D for
F being
BinOp of
D st ( for
A,
B being
Element of
Fin Y st
A misses B holds
F . (g . A),
(g . B) = g . (A \/ B) ) &
F is
commutative &
F is
associative &
F is
having_a_unity &
g . {} = the_unity_wrt F holds
for
I being
Element of
Fin X st ( for
x,
y being
set st
x in I &
y in I &
f . x meets f . y holds
x = y ) holds
(
F $$ I,
(g * f) = F $$ (f .: I),
g &
F $$ (f .: I),
g = g . (union (f .: I)) &
union (f .: I) is
Element of
Fin Y )
begin
definition
let i,
j,
n be
Nat;
let K be
Field;
let M be
Matrix of
n,;
assume that A1:
i in Seg n
and A2:
j in Seg n
;
func Delete M,
i,
j -> Matrix of
n -' 1,
equals :
Def1:
Deleting M,
i,
j;
coherence
Deleting M,i,j is Matrix of n -' 1,
end;
:: deftheorem Def1 defines Delete LAPLACE:def 1 :
theorem Th13:
for
n being
Nat for
K being
Field for
M being
Matrix of
n,
for
i,
j being
Nat st
i in Seg n &
j in Seg n holds
for
k,
m being
Nat st
k in Seg (n -' 1) &
m in Seg (n -' 1) holds
( (
k < i &
m < j implies
(Delete M,i,j) * k,
m = M * k,
m ) & (
k < i &
m >= j implies
(Delete M,i,j) * k,
m = M * k,
(m + 1) ) & (
k >= i &
m < j implies
(Delete M,i,j) * k,
m = M * (k + 1),
m ) & (
k >= i &
m >= j implies
(Delete M,i,j) * k,
m = M * (k + 1),
(m + 1) ) )
theorem Th14:
theorem Th15:
definition
let c,
n,
m be
Nat;
let D be non
empty set ;
let M be
Matrix of
n,
m,
D;
let pD be
FinSequence of
D;
func ReplaceCol M,
c,
pD -> Matrix of
n,
m,
D means :
Def2:
(
len it = len M &
width it = width M & ( for
i,
j being
Nat st
[i,j] in Indices M holds
( (
j <> c implies
it * i,
j = M * i,
j ) & (
j = c implies
it * i,
c = pD . i ) ) ) )
if len pD = len M otherwise it = M;
consistency
for b1 being Matrix of n,m,D holds verum
;
existence
( ( len pD = len M implies ex b1 being Matrix of n,m,D st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b1 * i,j = M * i,j ) & ( j = c implies b1 * i,c = pD . i ) ) ) ) ) & ( not len pD = len M implies ex b1 being Matrix of n,m,D st b1 = M ) )
uniqueness
for b1, b2 being Matrix of n,m,D holds
( ( len pD = len M & len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b1 * i,j = M * i,j ) & ( j = c implies b1 * i,c = pD . i ) ) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b2 * i,j = M * i,j ) & ( j = c implies b2 * i,c = pD . i ) ) ) implies b1 = b2 ) & ( not len pD = len M & b1 = M & b2 = M implies b1 = b2 ) )
end;
:: deftheorem Def2 defines ReplaceCol LAPLACE:def 2 :
for
c,
n,
m being
Nat for
D being non
empty set for
M being
Matrix of
n,
m,
D for
pD being
FinSequence of
D for
b7 being
Matrix of
n,
m,
D holds
( (
len pD = len M implies (
b7 = ReplaceCol M,
c,
pD iff (
len b7 = len M &
width b7 = width M & ( for
i,
j being
Nat st
[i,j] in Indices M holds
( (
j <> c implies
b7 * i,
j = M * i,
j ) & (
j = c implies
b7 * i,
c = pD . i ) ) ) ) ) ) & ( not
len pD = len M implies (
b7 = ReplaceCol M,
c,
pD iff
b7 = M ) ) );
theorem
for
n,
m,
c being
Nat for
D being non
empty set for
AD being
Matrix of
n,
m,
D for
pD being
FinSequence of
D for
i being
Nat st
i in Seg (width AD) holds
( (
i = c &
len pD = len AD implies
Col (RCol AD,c,pD),
i = pD ) & (
i <> c implies
Col (RCol AD,c,pD),
i = Col AD,
i ) )
theorem
theorem
theorem Th19:
for
n,
m,
c being
Nat for
D being non
empty set for
pD being
FinSequence of
D for
A being
Matrix of
n,
m,
D for
A' being
Matrix of
m,
n,
D st
A' = A @ & (
m = 0 implies
n = 0 ) holds
ReplaceCol A,
c,
pD = (ReplaceLine A',c,pD) @
begin
definition
let i,
n be
Nat;
let perm be
Element of
Permutations (n + 1);
assume A1:
i in Seg (n + 1)
;
func Rem perm,
i -> Element of
Permutations n means :
Def3:
for
k being
Nat st
k in Seg n holds
( (
k < i implies ( (
perm . k < perm . i implies
it . k = perm . k ) & (
perm . k >= perm . i implies
it . k = (perm . k) - 1 ) ) ) & (
k >= i implies ( (
perm . (k + 1) < perm . i implies
it . k = perm . (k + 1) ) & (
perm . (k + 1) >= perm . i implies
it . k = (perm . (k + 1)) - 1 ) ) ) );
existence
ex b1 being Element of Permutations n st
for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b1 . k = perm . k ) & ( perm . k >= perm . i implies b1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b1 . k = (perm . (k + 1)) - 1 ) ) ) )
uniqueness
for b1, b2 being Element of Permutations n st ( for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b1 . k = perm . k ) & ( perm . k >= perm . i implies b1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b1 . k = (perm . (k + 1)) - 1 ) ) ) ) ) & ( for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b2 . k = perm . k ) & ( perm . k >= perm . i implies b2 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b2 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b2 . k = (perm . (k + 1)) - 1 ) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines Rem LAPLACE:def 3 :
for
i,
n being
Nat for
perm being
Element of
Permutations (n + 1) st
i in Seg (n + 1) holds
for
b4 being
Element of
Permutations n holds
(
b4 = Rem perm,
i iff for
k being
Nat st
k in Seg n holds
( (
k < i implies ( (
perm . k < perm . i implies
b4 . k = perm . k ) & (
perm . k >= perm . i implies
b4 . k = (perm . k) - 1 ) ) ) & (
k >= i implies ( (
perm . (k + 1) < perm . i implies
b4 . k = perm . (k + 1) ) & (
perm . (k + 1) >= perm . i implies
b4 . k = (perm . (k + 1)) - 1 ) ) ) ) );
theorem Th20:
theorem Th21:
theorem Th22:
begin
:: deftheorem defines Minor LAPLACE:def 4 :
definition
let i,
j,
n be
Nat;
let K be
Field;
let M be
Matrix of
n,;
func Cofactor M,
i,
j -> Element of
equals
((power K) . (- (1_ K)),(i + j)) * (Minor M,i,j);
coherence
((power K) . (- (1_ K)),(i + j)) * (Minor M,i,j) is Element of
;
end;
:: deftheorem defines Cofactor LAPLACE:def 5 :
theorem Th23:
theorem Th24:
definition
let n be
Nat;
let K be
Field;
let M be
Matrix of
n,;
func Matrix_of_Cofactor M -> Matrix of
n,
means :
Def6:
for
i,
j being
Nat st
[i,j] in Indices it holds
it * i,
j = Cofactor M,
i,
j;
existence
ex b1 being Matrix of n, st
for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = Cofactor M,i,j
uniqueness
for b1, b2 being Matrix of n, st ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = Cofactor M,i,j ) & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * i,j = Cofactor M,i,j ) holds
b1 = b2
end;
:: deftheorem Def6 defines Matrix_of_Cofactor LAPLACE:def 6 :
begin
definition
let n,
i be
Nat;
let K be
Field;
let M be
Matrix of
n,;
func LaplaceExpL M,
i -> FinSequence of
means :
Def7:
(
len it = n & ( for
j being
Nat st
j in dom it holds
it . j = (M * i,j) * (Cofactor M,i,j) ) );
existence
ex b1 being FinSequence of st
( len b1 = n & ( for j being Nat st j in dom b1 holds
b1 . j = (M * i,j) * (Cofactor M,i,j) ) )
uniqueness
for b1, b2 being FinSequence of st len b1 = n & ( for j being Nat st j in dom b1 holds
b1 . j = (M * i,j) * (Cofactor M,i,j) ) & len b2 = n & ( for j being Nat st j in dom b2 holds
b2 . j = (M * i,j) * (Cofactor M,i,j) ) holds
b1 = b2
end;
:: deftheorem Def7 defines LaplaceExpL LAPLACE:def 7 :
definition
let n,
j be
Nat;
let K be
Field;
let M be
Matrix of
n,;
func LaplaceExpC M,
j -> FinSequence of
means :
Def8:
(
len it = n & ( for
i being
Nat st
i in dom it holds
it . i = (M * i,j) * (Cofactor M,i,j) ) );
existence
ex b1 being FinSequence of st
( len b1 = n & ( for i being Nat st i in dom b1 holds
b1 . i = (M * i,j) * (Cofactor M,i,j) ) )
uniqueness
for b1, b2 being FinSequence of st len b1 = n & ( for i being Nat st i in dom b1 holds
b1 . i = (M * i,j) * (Cofactor M,i,j) ) & len b2 = n & ( for i being Nat st i in dom b2 holds
b2 . i = (M * i,j) * (Cofactor M,i,j) ) holds
b1 = b2
end;
:: deftheorem Def8 defines LaplaceExpC LAPLACE:def 8 :
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem Th38:
begin
:: deftheorem defines * LAPLACE:def 9 :
:: deftheorem defines * LAPLACE:def 10 :
theorem
theorem