let n be Nat; :: thesis: for K being Field
for j being Nat
for M being Matrix of n,K st j in Seg n holds
Det M = Sum (LaplaceExpC M,j)
let K be Field; :: thesis: for j being Nat
for M being Matrix of n,K st j in Seg n holds
Det M = Sum (LaplaceExpC M,j)
let j be Nat; :: thesis: for M being Matrix of n,K st j in Seg n holds
Det M = Sum (LaplaceExpC M,j)
let M be Matrix of n,K; :: thesis: ( j in Seg n implies Det M = Sum (LaplaceExpC M,j) )
assume A1: j in Seg n ; :: thesis: Det M = Sum (LaplaceExpC M,j)
thus Det M = Det (M @ ) by MATRIXR2:43
.= Sum (LaplaceExpL (M @ ),j) by A1, Th25
.= Sum (LaplaceExpC M,j) by A1, Th26 ; :: thesis: verum