Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

added theorem
deleted theorem alg_hom.finite_type.comp
deleted theorem
deleted def alg_hom.finite_type
deleted theorem algebra.finite_type.equiv
deleted theorem algebra.finite_type.self
deleted theorem algebra.finite_type.trans
deleted theorem ring_hom.finite_type.comp
deleted theorem