mathlib3

6e7ca692 - chore(ring_theory): split finiteness into finite, finite type and finite presentation (#17481)

chore(ring_theory): split finiteness into finite, finite type and finite 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.