chore(data/polynomial/*): delete, rename and move lemmas (#12852)

- Replace `eval_eq_finset_sum` and `eval_eq_finset_sum'` with `eval_eq_sum_range` and `eval_eq_sum_range'` which are consistent with `eval₂_eq_sum_range`, `eval₂_eq_sum_range'` `eval_eq_finset_sum`, `eval_eq_finset_sum'`. Notice that the type of `eval_eq_sum_range'` is different, but this lemma has not been used anywhere in mathlib.
- Move the lemma `C_eq_int_cast` from `data/polynomial/degree/definitions.lean` to `data/polynomial/basic.lean`. `C_eq_nat_cast` was already here.

Author: astrainfinita

src/analysis/special_functions/polynomials.lean

@@ -45,7 +45,7 @@ begin
   { simp [h] },
   { conv_lhs
     { funext,
-      rw [polynomial.eval_eq_finset_sum, sum_range_succ] },
+      rw [polynomial.eval_eq_sum_range, sum_range_succ] },
     exact is_equivalent.refl.add_is_o (is_o.sum $ λ i hi, is_o.const_mul_left
       (is_o.const_mul_right (λ hz, h $ leading_coeff_eq_zero.mp hz) $
         is_o_pow_pow_at_top_of_lt (mem_range.mp hi)) _) }

src/data/polynomial/algebra_map.lean

@@ -264,7 +264,7 @@ lemma aeval_eq_sum_range [algebra R S] {p : R[X]} (x : S) :
 by { simp_rw algebra.smul_def, exact eval₂_eq_sum_range (algebra_map R S) x }
 
 lemma aeval_eq_sum_range' [algebra R S] {p : R[X]} {n : ℕ} (hn : p.nat_degree < n) (x : S) :
-aeval x p = ∑ i in finset.range n, p.coeff i • x ^ i :=
+  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])
@@ -401,7 +401,7 @@ lemma aeval_endomorphism {M : Type*}
   aeval f p v = p.sum (λ n b, b • (f ^ n) v) :=
 begin
   rw [aeval_def, eval₂],
-  exact (linear_map.applyₗ v).map_sum ,
+  exact (linear_map.applyₗ v).map_sum,
 end
 
 end polynomial

src/data/polynomial/basic.lean

@@ -685,6 +685,10 @@ by rw [eq_neg_iff_add_eq_zero, ←monomial_add, neg_add_self, monomial_zero_righ
 @[simp] lemma support_neg {p : R[X]} : (-p).support = p.support :=
 by { rcases p, simp [support, neg_to_finsupp] }
 
+@[simp]
+lemma C_eq_int_cast (n : ℤ) : C (n : R) = n :=
+(C : R →+* _).map_int_cast n
+
 end ring
 
 instance [comm_ring R] : comm_ring R[X] :=

src/data/polynomial/degree/definitions.lean

@@ -371,9 +371,6 @@ lemma coeff_mul_X_sub_C {p : R[X]} {r : R} {a : ℕ} :
   coeff (p * (X - C r)) (a + 1) = coeff p a - coeff p (a + 1) * r :=
 by simp [mul_sub]
 
-lemma C_eq_int_cast (n : ℤ) : C (n : R) = n :=
-(C : R →+* _).map_int_cast n
-
 @[simp] lemma degree_neg (p : R[X]) : degree (-p) = degree p :=
 by unfold degree; rw support_neg
 

src/data/polynomial/eval.lean

@@ -242,16 +242,13 @@ def eval : R → R[X] → R := eval₂ (ring_hom.id _)
 lemma eval_eq_sum : p.eval x = p.sum (λ e a, a * x ^ e) :=
 rfl
 
-lemma eval_eq_finset_sum (p : R[X]) (x : R) :
-  p.eval x = ∑ i in range (p.nat_degree + 1), p.coeff i * x ^ i :=
-by { rw [eval_eq_sum, sum_over_range], simp }
+lemma eval_eq_sum_range {p : R[X]} (x : R) :
+  p.eval x = ∑ i in finset.range (p.nat_degree + 1), p.coeff i * x ^ i :=
+by rw [eval_eq_sum, sum_over_range]; simp
 
-lemma eval_eq_finset_sum' (P : R[X]) :
-  (λ x, eval x P) = (λ x, ∑ i in range (P.nat_degree + 1), P.coeff i * x ^ i) :=
-begin
-  ext,
-  exact P.eval_eq_finset_sum x
-end
+lemma eval_eq_sum_range' {p : R[X]} {n : ℕ} (hn : p.nat_degree < n) (x : R) :
+  p.eval x = ∑ i in finset.range n, p.coeff i * x ^ i :=
+by rw [eval_eq_sum, p.sum_over_range' _ _ hn]; simp
 
 @[simp] lemma eval₂_at_apply {S : Type*} [semiring S] (f : R →+* S) (r : R) :
   p.eval₂ f (f r) = f (p.eval r) :=

src/data/polynomial/mirror.lean

@@ -98,7 +98,7 @@ end
 --TODO: Extract `finset.sum_range_rev_at` lemma.
 lemma mirror_eval_one : p.mirror.eval 1 = p.eval 1 :=
 begin
-  simp_rw [eval_eq_finset_sum, one_pow, mul_one, mirror_nat_degree],
+  simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_nat_degree],
   refine finset.sum_bij_ne_zero _ _ _ _ _,
   { exact λ n hn hp, rev_at (p.nat_degree + p.nat_trailing_degree) n },
   { intros n hn hp,

src/ring_theory/polynomial/eisenstein.lean

@@ -90,7 +90,7 @@ lemma exists_mem_adjoin_mul_eq_pow_nat_degree {x : S} (hx : aeval x f = 0)
   (hmo : f.monic) (hf : f.is_weakly_eisenstein_at P) : ∃ y ∈ adjoin R ({x} : set S),
   (algebra_map R S) p * y = x ^ (f.map (algebra_map R S)).nat_degree :=
 begin
-  rw [aeval_def, polynomial.eval₂_eq_eval_map, eval_eq_finset_sum, range_add_one,
+  rw [aeval_def, polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one,
     sum_insert not_mem_range_self, sum_range, (hmo.map
     (algebra_map R S)).coeff_nat_degree, one_mul] at hx,
   replace hx := eq_neg_of_add_eq_zero hx,
@@ -135,7 +135,7 @@ begin
   rw [hk, pow_add],
   suffices : x ^ f.nat_degree ∈ 𝓟,
   { exact mul_mem_right (x ^ k) 𝓟 this },
-  rw [is_root.def, eval_eq_finset_sum, finset.range_add_one, finset.sum_insert
+  rw [is_root.def, eval_eq_sum_range, finset.range_add_one, finset.sum_insert
     finset.not_mem_range_self, finset.sum_range, hmo.coeff_nat_degree, one_mul] at hroot,
   rw [eq_neg_of_add_eq_zero hroot, neg_mem_iff],
   refine submodule.sum_mem _ (λ i hi,  mul_mem_right _ _ (hf.mem (fin.is_lt i)))