Move Properties of UnivariateList-Polynomials to CommRing

[felixwellen]

In Algebra.Polynomials, there are pointers to constructions of CommRing and CommAlgebras of polynomials and proofs on the relations between the different definitions. A notable exception is Polynomials.UnivariateList.Properties, which contains the construction of the CommRing structure and more properties. We could move that to the Instance in CommRing, to make everything more coherent.