polynomialFunctions

Stream: mathlib4

[Yury G. Kudryashov]

Should we generalize docs#polynomialFunctions to use docs#PolynomialModule ?

[Yury G. Kudryashov]

BTW, the docstring of docs#PolynomialModule should say somewhere that these are polynomials with variables in R and coefficients in M.

[Yury G. Kudryashov]

#xy: in #24566 I'm generalizing the Weierstrass approximation theorem (using Berstein polynomials) to C(I, E).