THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Multivariable polynomials on a type is the left adjoint of the
forgetful functor from commutative rings to types.
The free functor
Type u ⥤ CommRing sending a type
X to the multivariable (commutative)
polynomials with variables
x : X.
The free-forgetful adjunction for commutative rings.