Commit 2022-11-15 00:06 6e7ca692

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.