lemma names in data/polynomial

Stream: general

[FR]

We have

lemma eval₂_eq_sum_range :
  p.eval₂ f x = ∑ i in finset.range (p.nat_degree + 1), f (p.coeff i) * x^i
lemma eval₂_eq_sum_range' (f : R →+* S) {p : R[X]} {n : ℕ} (hn : p.nat_degree < n) (x : S) :
  eval₂ f x p = ∑ i in finset.range n, f (p.coeff i) * x ^ i
lemma aeval_eq_sum_range [algebra R S] {p : R[X]} (x : S) :
  aeval x p = ∑ i in finset.range (p.nat_degree + 1), p.coeff i • x ^ i
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

and

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
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)

Looks like there are some inconsistencies.

[FR]

Would it be better to replace eval_eq_finset_sum and eval_eq_finset_sum' with the following lemmas?

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
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

[Kevin Buzzard]

docs#polynomial.eval_eq_finset_sum

[Kevin Buzzard]

eval_eq_sum_range looks the same as that to me -- is your question about renaming the lemmas or did I miss something?

[FR]

Yes, there are some inconsistencies in names. See the previous comment.