# Adjoining elements to form subalgebras: relation to polynomials #

In this file we prove a few results representing algebra.adjoin R s as the range of mv_polynomial.aeval or polynomial.aeval.