feat(linear_algebra/matrix/rank): generalize to rings (#18748)
This addresses a TODO comment.
To achieve this we generalize `submodule.finrank_le`, `submodule.finrank_quotient_le`, and `finrank_le_finrank_of_injective` from vector spaces to free modules, and add a new lemma `linear_map.finrank_range_le`.
