theorem :: MATRIX13:101

for K being Field
for M being diagonal Matrix of K
for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
the_rank_of M = card NonZero1