theorem LinearAlgebra.rank_transpose {F : Type u_1} [Field F] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (M : Matrix m n F) : M.rank = M.transpose.rank