theorem :: MATRIX13:84

for K being Field
for M being Matrix of K holds the_rank_of M = the_rank_of (M @)