chore(ring_theory/polynomial/bernstein): use ∑ notation (#11060)

Also rewrite a proof using `calc` mode

src/ring_theory/polynomial/bernstein.lean

@@ -36,6 +36,7 @@ noncomputable theory
 
 open nat (choose)
 open polynomial (X)
+open_locale big_operators
 
 variables (R : Type*) [comm_ring R]
 
@@ -291,20 +292,16 @@ lemma linear_independent (n : ℕ) :
   linear_independent ℚ (λ ν : fin (n+1), bernstein_polynomial ℚ n ν) :=
 linear_independent_aux n (n+1) (le_refl _)
 
-lemma sum (n : ℕ) : (finset.range (n + 1)).sum (λ ν, bernstein_polynomial R n ν) = 1 :=
-begin
-  -- We calculate `(x + (1-x))^n` in two different ways.
-  conv { congr, congr, skip, funext, dsimp [bernstein_polynomial], rw [mul_assoc, mul_comm], },
-  rw ←add_pow,
-  simp,
-end
-
+lemma sum (n : ℕ) : ∑ ν in finset.range (n + 1), bernstein_polynomial R n ν = 1 :=
+calc ∑ ν in finset.range (n + 1), bernstein_polynomial R n ν = (X + (1 - X)) ^ n :
+  by { rw add_pow, simp only [bernstein_polynomial, mul_comm, mul_assoc, mul_left_comm] }
+... = 1 : by simp
 
 open polynomial
 open mv_polynomial
 
 lemma sum_smul (n : ℕ) :
-  (finset.range (n + 1)).sum (λ ν, ν • bernstein_polynomial R n ν) = n • X :=
+  ∑ ν in finset.range (n + 1), ν • bernstein_polynomial R n ν = n • X :=
 begin
   -- We calculate the `x`-derivative of `(x+y)^n`, evaluated at `y=(1-x)`,
   -- either directly or by using the binomial theorem.
@@ -353,8 +350,7 @@ begin
 end
 
 lemma sum_mul_smul (n : ℕ) :
-  (finset.range (n + 1)).sum (λ ν, (ν * (ν-1)) • bernstein_polynomial R n ν) =
-    (n * (n-1)) • X^2 :=
+  ∑ ν in finset.range (n + 1), (ν * (ν-1)) • bernstein_polynomial R n ν = (n * (n-1)) • X^2 :=
 begin
   -- We calculate the second `x`-derivative of `(x+y)^n`, evaluated at `y=(1-x)`,
   -- either directly or by using the binomial theorem.
@@ -413,7 +409,7 @@ A certain linear combination of the previous three identities,
 which we'll want later.
 -/
 lemma variance (n : ℕ) :
-  (finset.range (n+1)).sum (λ ν, (n • polynomial.X - ν)^2 * bernstein_polynomial R n ν) =
+  ∑ ν in finset.range (n+1), (n • polynomial.X - ν)^2 * bernstein_polynomial R n ν =
     n • polynomial.X * (1 - polynomial.X) :=
 begin
   have p :