feat(data/polynomial/algebra_map): remove some lemmas about aeval, …

…add `protected` on `polynomial.map_list_prod` (#13294)

Remove `aeval_sum` which is a duplicate of `map_sum`.
Remove `aeval_prod` which is a duplicate of `map_prod`.

src/data/polynomial/algebra_map.lean

@@ -273,15 +273,6 @@ lemma aeval_eq_sum_range' [algebra R S] {p : R[X]} {n : ℕ} (hn : p.nat_degree
   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 : ι → R[X])
-  (g : S) : aeval g (∑ i in s, f i) = ∑ i in s, aeval g (f i) :=
-(polynomial.aeval g : R[X] →ₐ[_] _).map_sum f s
-
-@[to_additive]
-lemma aeval_prod {ι : Type*} [algebra R S] (s : finset ι)
-  (f : ι → R[X]) (g : S) : aeval g (∏ i in s, f i) = ∏ i in s, aeval g (f i) :=
-(polynomial.aeval g : R[X] →ₐ[_] _).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

src/data/polynomial/eval.lean

@@ -237,7 +237,7 @@ zero_dvd_iff.mp (h0 ▸ eval₂_dvd f x h)
 
 lemma eval₂_list_prod (l : list R[X]) (x : S) :
   eval₂ f x l.prod = (l.map (eval₂ f x)).prod :=
-_root_.map_list_prod (eval₂_ring_hom f x) l
+map_list_prod (eval₂_ring_hom f x) l
 
 end eval₂
 
@@ -624,7 +624,7 @@ ring_hom.ext $ λ x, map_id
   (map_ring_hom f).comp (map_ring_hom g) = map_ring_hom (f.comp g) :=
 ring_hom.ext $ polynomial.map_map g f
 
-lemma map_list_prod (L : list R[X]) : L.prod.map f = (L.map $ map f).prod :=
+protected lemma map_list_prod (L : list R[X]) : L.prod.map f = (L.map $ map f).prod :=
 eq.symm $ list.prod_hom _ (map_ring_hom f).to_monoid_hom
 
 @[simp] protected lemma map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n :=
@@ -766,11 +766,11 @@ lemma root_mul_right_of_is_root {p : R[X]} (q : R[X]) :
 
 lemma eval₂_multiset_prod (s : multiset R[X]) (x : S) :
   eval₂ f x s.prod = (s.map (eval₂ f x)).prod :=
-_root_.map_multiset_prod (eval₂_ring_hom f x) s
+map_multiset_prod (eval₂_ring_hom f x) s
 
 lemma eval₂_finset_prod (s : finset ι) (g : ι → R[X]) (x : S) :
   (∏ i in s, g i).eval₂ f x = ∏ i in s, (g i).eval₂ f x :=
-_root_.map_prod (eval₂_ring_hom f x) _ _
+map_prod (eval₂_ring_hom f x) _ _
 
 /--
 Polynomial evaluation commutes with `list.prod`