for n being Nat
for K being Field
for M being Matrix of n,K holds
( the_rank_of M = n iff Det M <> 0. K )