Commit 2020-12-12 17:17 5ced4dde

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.