theorem :: MATRIX13:95

for K being Field
for M being Matrix of K holds
( the_rank_of M = 0 iff M = 0. (K,(len M),(width M)) )