Commit 2022-11-12 05:40 019ead10

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.