chore(linear_algebra/dimension): deduplicate lemmas (#18743)
We have some lemmas in the `module.free` namespace which duplicate lemmas in the root namespace. This moves all the remaining `rank` lemmas in this namespace into the root namespace, and cleans up the overlapping lemmas this creates.
The changes are:
* `module.free.rank_eq_card_choose_basis_index`: unchanged but moved to an earlier file
* `rank_prod` → `rank_prod'` (the non-universe polymorphic version)
* `module.free.rank_prod` → `rank_prod`
* none → `rank_finsupp` (new lemma)
* `finsupp.rank_eq` → `rank_finsupp'` (the non-universe polymorphic version)
* `module.free.rank_finsupp` → `rank_finsupp_self`
* `module.free.rank_finsupp'` → `rank_finsupp_self'` (the non-universe polymorphic version)
* `module.free.rank_pi_finite` → `rank_pi` (these were duplicates)
* For everything else, `module.free.rank_*` → `rank_*`
