feat(ring_theory/finiteness): add `mv_polynomial_of_finite_presentation` (#6512)
Add `mv_polynomial_of_finite_presentation`: the polynomial ring over a finitely presented algebra is finitely presented.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>