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