mathlib3

019ead10 - chore(linear_algebra): remove `finite_dimensional` import from `finsupp_vector_space` (#17474)

chore(linear_algebra): remove `finite_dimensional` import from `finsupp_vector_space` (#17474) This PR removes `linear_algebra/finite_dimensional.lean` from the imports of `linear_algebra/finsupp_vector_space.lean`. It turns out the only results that needed this import can already be done in `linear_algebra/finite_dimensional.lean` so I just moved it over. The purpose of this change is to insert `linear_algebra/free_module/finite.lean` in between `linear_algebra/finrank.lean` and `linear_algebra/finite_dimensional.lean`, as discussed in the module docs for `linear_algebra/free_module/finite.lean` and in #17401.