Continuity of algebra evaluation of multivariate polynomials

For a commutative semiring k, a topological commutative k-algebra R whose ring operations are continuous, and a polynomial p in variables indexed by an arbitrary type σ with coefficients in k, the function v ↦ aeval v p on σ → R is continuous. This is the multivariate, algebra-valued form of Mathlib's Polynomial.continuous_aeval; Mathlib's MvPolynomial.continuous_eval treats only polynomials with coefficients in R itself.

theorem MvPolynomial.continuous_aeval {k : Type u_1} {R : Type u_2} {σ : Type u_3} [CommSemiring k] [CommSemiring R] [Algebra k R] [TopologicalSpace R] [IsTopologicalSemiring R] (p : MvPolynomial σ k) : Continuous fun (v : σ → R) => (aeval v) p

Evaluating a polynomial with coefficients in k at points of a topological k-algebra R with continuous ring operations is continuous, for any set of variables.