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

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