let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Det M = 0. K
let K be Field; :: thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Det M = 0. K
let M be Matrix of n,K; :: thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies Det M = 0. K )
assume A1: ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; :: thesis: Det M = 0. K
set f = Path_product M;
set F = the addF of K;
Det M = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) by MATRIX_3:def 9
.= 0. K by A1, Th51 ;
hence Det M = 0. K ; :: thesis: verum