:: deftheorem Def4 defines the_rank_of MATRIX13:def 4 :
for K being Field
for M being Matrix of K
for b₃ being Element of NAT holds
( b₃ = the_rank_of M iff ( ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = b₃ & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b₃ ) ) );