feat(data/(mv_)polynomial): add aeval_prod and aeval_sum for (mv_)pol…

…ynomial (#10594)

Another couple of small polynomial helper lemmas from flt-regular.

src/data/mv_polynomial/basic.lean

@@ -1095,6 +1095,15 @@ lemma aeval_eq_zero [algebra R S₂] (f : σ → S₂) (φ : mv_polynomial σ R)
   aeval f φ = 0 :=
 eval₂_hom_eq_zero _ _ _ h
 
+lemma aeval_sum {ι : Type*} (s : finset ι) (φ : ι → mv_polynomial σ R) :
+  aeval f (∑ i in s, φ i) = ∑ i in s, aeval f (φ i) :=
+(mv_polynomial.aeval f).map_sum _ _
+
+@[to_additive]
+lemma aeval_prod {ι : Type*} (s : finset ι) (φ : ι → mv_polynomial σ R) :
+  aeval f (∏ i in s, φ i) = ∏ i in s, aeval f (φ i) :=
+(mv_polynomial.aeval f).map_prod _ _
+
 end aeval
 
 section aeval_tower

src/data/polynomial/algebra_map.lean

@@ -260,6 +260,15 @@ lemma aeval_eq_sum_range' [algebra R S] {p : polynomial R} {n : ℕ} (hn : p.nat
 aeval x p = ∑ i in finset.range n, p.coeff i • x ^ i :=
 by { simp_rw algebra.smul_def, exact eval₂_eq_sum_range' (algebra_map R S) hn x }
 
+lemma aeval_sum {ι : Type*} [algebra R S] (s : finset ι) (f : ι → polynomial R)
+  (g : S) : aeval g (∑ i in s, f i) = ∑ i in s, aeval g (f i) :=
+(polynomial.aeval g : polynomial R →ₐ[_] _).map_sum f s
+
+@[to_additive]
+lemma aeval_prod {ι : Type*} [algebra R S] (s : finset ι)
+  (f : ι → polynomial R) (g : S) : aeval g (∏ i in s, f i) = ∏ i in s, aeval g (f i) :=
+(polynomial.aeval g : polynomial R →ₐ[_] _).map_prod f s
+
 lemma is_root_of_eval₂_map_eq_zero
   (hf : function.injective f) {r : R} : eval₂ f (f r) p = 0 → p.is_root r :=
 begin