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