:: deftheorem Def8 defines LaplaceExpC LAPLACE:def 8 :
for n, j being Nat
for K being Field
for M being Matrix of n,K
for b₅ being FinSequence of K holds
( b₅ = LaplaceExpC (M,j) iff ( len b₅ = n & ( for i being Nat st i in dom b₅ holds
b₅ . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ) );