chore(ring_theory): split finiteness into finite, finite type and fin…

…ite presentation (#17481)

`module.finite` is used in a lot of places (especially in the form of `finite_dimensional`) but it is defined alongside `algebra.finite_type` and `algebra.finite_presentation`, so it brings a lot of dependencies with it. By splitting the file along the lines of the three definitions we should be able to clean up the import graph noticeably. In particular, finite dimensional vector spaces shouldn't know about (`mv_`)polynomials anymore.

src/data/polynomial/module.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 
-import ring_theory.finiteness
+import ring_theory.finite_type
 
 /-!
 # Polynomial module

src/linear_algebra/finite_dimensional.lean

@@ -6,6 +6,7 @@ Authors: Chris Hughes
 import algebra.algebra.subalgebra.basic
 import field_theory.finiteness
 import linear_algebra.finrank
+import tactic.interval_cases
 
 /-!
 # Finite dimensional vector spaces

src/ring_theory/adjoin_root.lean

@@ -7,6 +7,8 @@ import algebra.algebra.basic
 import data.polynomial.field_division
 import linear_algebra.finite_dimensional
 import ring_theory.adjoin.basic
+import ring_theory.finite_presentation
+import ring_theory.finite_type
 import ring_theory.power_basis
 import ring_theory.principal_ideal_domain