chore(linear_algebra): remove finite_dimensional import from `finsu…

…pp_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.

src/field_theory/mv_polynomial.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 
+import data.mv_polynomial.comm_ring
 import ring_theory.mv_polynomial.basic
 
 /-!

src/linear_algebra/finite_dimensional.lean

@@ -1497,3 +1497,33 @@ end
 
 end End
 end module
+
+section module
+
+open module
+
+open_locale cardinal
+
+lemma cardinal_mk_eq_cardinal_mk_field_pow_dim
+  (K V : Type u) [field K] [add_comm_group V] [module K V] [finite_dimensional K V] :
+  #V = #K ^ module.rank K V :=
+begin
+  let s := basis.of_vector_space_index K V,
+  let hs := basis.of_vector_space K V,
+  calc #V = #(s →₀ K) : quotient.sound ⟨hs.repr.to_equiv⟩
+    ... = #(s → K) : quotient.sound ⟨finsupp.equiv_fun_on_fintype⟩
+    ... = _ : by rw [← cardinal.lift_inj.1 hs.mk_eq_dim, cardinal.power_def]
+end
+
+lemma cardinal_lt_aleph_0_of_finite_dimensional
+  (K V : Type u) [field K] [add_comm_group V] [module K V]
+  [_root_.finite K] [finite_dimensional K V] :
+  #V < ℵ₀ :=
+begin
+  letI : is_noetherian K V := is_noetherian.iff_fg.2 infer_instance,
+  rw cardinal_mk_eq_cardinal_mk_field_pow_dim K V,
+  exact cardinal.power_lt_aleph_0 (cardinal.lt_aleph_0_of_finite K)
+    (is_noetherian.dim_lt_aleph_0 K V),
+end
+
+end module

src/linear_algebra/finsupp_vector_space.lean

@@ -5,7 +5,6 @@ Authors: Johannes Hölzl
 -/
 
 import linear_algebra.dimension
-import linear_algebra.finite_dimensional
 import linear_algebra.std_basis
 
 /-!
@@ -14,8 +13,7 @@ import linear_algebra.std_basis
 This file contains results on the `R`-module structure on functions of finite support from a type
 `ι` to an `R`-module `M`, in particular in the case that `R` is a field.
 
-Furthermore, it contains some facts about isomorphisms of vector spaces from equality of dimension
-as well as the cardinality of finite dimensional vector spaces.
+Furthermore, it contains some facts about isomorphisms of vector spaces from equality of dimension.
 
 ## TODO
 
@@ -184,33 +182,6 @@ end
 
 end module
 
-section module
-
-open module
-
-variables (K V : Type u) [field K] [add_comm_group V] [module K V]
-
-lemma cardinal_mk_eq_cardinal_mk_field_pow_dim [finite_dimensional K V] :
-  #V = #K ^ module.rank K V :=
-begin
-  let s := basis.of_vector_space_index K V,
-  let hs := basis.of_vector_space K V,
-  calc #V = #(s →₀ K) : quotient.sound ⟨hs.repr.to_equiv⟩
-    ... = #(s → K) : quotient.sound ⟨finsupp.equiv_fun_on_fintype⟩
-    ... = _ : by rw [← cardinal.lift_inj.1 hs.mk_eq_dim, cardinal.power_def]
-end
-
-lemma cardinal_lt_aleph_0_of_finite_dimensional [_root_.finite K] [finite_dimensional K V] :
-  #V < ℵ₀ :=
-begin
-  letI : is_noetherian K V := is_noetherian.iff_fg.2 infer_instance,
-  rw cardinal_mk_eq_cardinal_mk_field_pow_dim K V,
-  exact cardinal.power_lt_aleph_0 (cardinal.lt_aleph_0_of_finite K)
-    (is_noetherian.dim_lt_aleph_0 K V),
-end
-
-end module
-
 namespace basis
 
 variables {R M n : Type*}

src/ring_theory/localization/module.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu, Anne Baanen
 -/
-import linear_algebra.linear_independent
+import linear_algebra.basis
 import ring_theory.localization.fraction_ring
 import ring_theory.localization.integer
 

src/ring_theory/mv_polynomial/basic.lean

@@ -5,6 +5,8 @@ Authors: Johannes Hölzl
 -/
 
 import algebra.char_p.basic
+import data.polynomial.algebra_map
+import data.mv_polynomial.variables
 import linear_algebra.finsupp_vector_space
 
 /-!

src/ring_theory/tensor_product.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johan Commelin
 -/
 
+import linear_algebra.finite_dimensional
 import linear_algebra.tensor_product_basis
 import ring_theory.adjoin.basic