mathlib3

5ced4dde - feat(ring_theory/finiteness): add iff_quotient_mv_polynomial (#5321)

feat(ring_theory/finiteness): add iff_quotient_mv_polynomial (#5321) Add characterizations of finite type algebra as quotient of polynomials rings. There are three version of the same lemma, using a `finset`, a `fintype` and `fin n`.