theorem Th76: :: MATRIX13:76

for K being Field
for M being Matrix of K
for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm (M,rt1,rt2)) <> 0. K ) & ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds
n <= RANK ) ) )