theorem :: MATRIX13:86
for K being Field
for a being Element of K
for M being Matrix of K st a <> 0. K holds
the_rank_of M = the_rank_of (a * M)