feat(linear_algebra/dimension): free generalizations (#18722)
Generalizes many results about `module.rank` from `[division_ring K]` to `[ring K] [strong_rank_condition K] [module.free K V]`.
Some lemmas have been moved around in the file to make use of existing `variables` groupings.
There are some lemmas about division rings that I wasn't able to weaken the assumptions on.
I'll make the corresponding generalizations to `finrank` in a follow-up PR.
