# Commit 2022-11-15 00:06 6e7ca692

View on Github →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.