mathlib

21407283 - feat(data/matrix/rank): rank of a matrix is the rank of its column space (#18778)

feat(data/matrix/rank): rank of a matrix is the rank of its column space (#18778) This is a TODO comment in this file left from #10826. Proving the link to the row space is harder, and only easy to prove for `is_R_or_C`; so I've left it for another time.