chore(*): use prod notation (#2989)

The biggest field test of the new product notation.

Author: kckennylau

src/analysis/analytic/basic.lean

@@ -69,7 +69,7 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 {F : Type*} [normed_group F] [normed_space 𝕜 F]
 {G : Type*} [normed_group G] [normed_space 𝕜 G]
 
-open_locale topological_space classical
+open_locale topological_space classical big_operators
 open filter
 
 /-! ### The radius of a formal multilinear series -/
@@ -333,7 +333,7 @@ begin
   apply norm_sub_le_of_geometric_bound_of_has_sum ha _ (hf.has_sum this),
   assume n,
   calc ∥(p n) (λ (i : fin n), y)∥
-    ≤ ∥p n∥ * (finset.univ.prod (λ i : fin n, ∥y∥)) : continuous_multilinear_map.le_op_norm _ _
+    ≤ ∥p n∥ * (∏ i : fin n, ∥y∥) : continuous_multilinear_map.le_op_norm _ _
     ... = nnnorm (p n) * (nnnorm y)^n : by simp
     ... ≤ nnnorm (p n) * r' ^ n :
       mul_le_mul_of_nonneg_left (pow_le_pow_of_le_left (nnreal.coe_nonneg _) (le_of_lt yr') _)
@@ -431,7 +431,7 @@ lemma formal_multilinear_series.has_fpower_series_on_ball [complete_space F]
     refine (summable_of_norm_bounded (λ n, (C : ℝ) * a ^ n)
       ((summable_geometric_of_lt_1 a.2 ha).mul_left _) (λ n, _)).has_sum,
     calc ∥(p n) (λ (i : fin n), y)∥
-      ≤ ∥p n∥ * (finset.univ.prod (λ i : fin n, ∥y∥)) : continuous_multilinear_map.le_op_norm _ _
+      ≤ ∥p n∥ * (∏ i : fin n, ∥y∥) : continuous_multilinear_map.le_op_norm _ _
       ... = nnnorm (p n) * (nnnorm y)^n : by simp
       ... ≤ C * a ^ n : by exact_mod_cast hC n
   end }

src/analysis/convex/specific_functions.lean

@@ -21,6 +21,7 @@ In this file we prove that the following functions are convex:
 -/
 
 open real set
+open_locale big_operators
 
 /-- `exp` is convex on the whole real line -/
 lemma convex_on_exp : convex_on univ exp :=
@@ -53,15 +54,15 @@ lemma finset.prod_nonneg_of_card_nonpos_even
   {α β : Type*} [linear_ordered_comm_ring β]
   {f : α → β} [decidable_pred (λ x, f x ≤ 0)]
   {s : finset α} (h0 : (s.filter (λ x, f x ≤ 0)).card.even) :
-  0 ≤ s.prod f :=
-calc 0 ≤ s.prod (λ x, (if f x ≤ 0 then (-1:β) else 1) * f x) :
+  0 ≤ ∏ x in s, f x :=
+calc 0 ≤ (∏ x in s, ((if f x ≤ 0 then (-1:β) else 1) * f x)) :
   finset.prod_nonneg (λ x _, by
     { split_ifs with hx hx, by simp [hx], simp at hx ⊢, exact le_of_lt hx })
 ... = _ : by rw [finset.prod_mul_distrib, finset.prod_ite, finset.prod_const_one,
   mul_one, finset.prod_const, neg_one_pow_eq_pow_mod_two, nat.even_iff.1 h0, pow_zero, one_mul]
 
 lemma int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : n.even) :
-  0 ≤ (finset.range n).prod (λ k, m - k) :=
+  0 ≤ ∏ k in finset.range n, (m - k) :=
 begin
   cases (le_or_lt ↑n m) with hnm hmn,
   { exact finset.prod_nonneg (λ k hk, sub_nonneg.2 (le_trans

src/analysis/mean_inequalities.lean

@@ -30,19 +30,19 @@ and `n=3`.
 universes u v
 
 open real finset
-open_locale classical nnreal
+open_locale classical nnreal big_operators
 
 variables {ι : Type u} (s : finset ι)
 
 /-- Geometric mean is less than or equal to the arithmetic mean, weighted version
 for functions on `finset`s. -/
 theorem real.am_gm_weighted (w z : ι → ℝ)
   (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : s.sum w = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :
-  s.prod (λ i, (z i) ^ (w i)) ≤ s.sum (λ i, w i * z i) :=
+  (∏ i in s, (z i) ^ (w i)) ≤ s.sum (λ i, w i * z i) :=
 begin
   let s' := s.filter (λ i, w i ≠ 0),
   rw [← sum_filter_ne_zero] at hw',
-  suffices : s'.prod (λ i, (z i) ^ (w i)) ≤ s'.sum (λ i, w i * z i),
+  suffices : (∏ i in s', (z i) ^ (w i)) ≤ s'.sum (λ i, w i * z i),
   { have A : ∀ i ∈ s, i ∉ s' → w i = 0,
     { intros i hi hi',
       simpa only [hi, mem_filter, ne.def, true_and, not_not] using hi' },
@@ -69,7 +69,7 @@ begin
 end
 
 theorem nnreal.am_gm_weighted (w z : ι → ℝ≥0) (hw' : s.sum w = 1) :
-  s.prod (λ i, (z i) ^ (w i:ℝ)) ≤ s.sum (λ i, w i * z i) :=
+  (∏ i in s, (z i) ^ (w i:ℝ)) ≤ s.sum (λ i, w i * z i) :=
 begin
   rw [← nnreal.coe_le_coe, nnreal.coe_prod, nnreal.coe_sum],
   refine real.am_gm_weighted _ _ _ (λ i _, (w i).coe_nonneg) _ (λ i _, (z i).coe_nonneg),

src/data/monoid_algebra.lean

@@ -36,7 +36,7 @@ seems impossible to use.
 -/
 
 noncomputable theory
-open_locale classical
+open_locale classical big_operators
 
 open finset finsupp
 
@@ -385,7 +385,7 @@ variable {ι : Type ui}
 
 lemma prod_single [comm_semiring k] [comm_monoid G]
   {s : finset ι} {a : ι → G} {b : ι → k} :
-  s.prod (λi, single (a i) (b i)) = single (s.prod a) (s.prod b) :=
+  (∏ i in s, single (a i) (b i)) = single (∏ i in s, a i) (∏ i in s, b i) :=
 finset.induction_on s rfl $ λ a s has ih, by rw [prod_insert has, ih,
   single_mul_single, prod_insert has, prod_insert has]
 
@@ -645,7 +645,7 @@ variable {ι : Type ui}
 
 lemma prod_single [comm_semiring k] [add_comm_monoid G]
   {s : finset ι} {a : ι → G} {b : ι → k} :
-  s.prod (λi, single (a i) (b i)) = single (s.sum a) (s.prod b) :=
+  (∏ i in s, single (a i) (b i)) = single (s.sum a) (∏ i in s, b i) :=
 finset.induction_on s rfl $ λ a s has ih, by rw [prod_insert has, ih,
   single_mul_single, sum_insert has, prod_insert has]
 

src/data/real/ennreal.lean

@@ -10,7 +10,7 @@ import data.set.intervals
 noncomputable theory
 open classical set
 
-open_locale classical
+open_locale classical big_operators
 variables {α : Type*} {β : Type*}
 
 /-- The extended nonnegative real numbers. This is usually denoted [0, ∞],
@@ -210,7 +210,7 @@ by simpa only [lt_top_iff_ne_top] using pow_ne_top
 of_nnreal_hom.map_sum f s
 
 @[simp, norm_cast] lemma coe_finset_prod {s : finset α} {f : α → nnreal} :
-  ↑(s.prod f) = (s.prod (λa, f a) : ennreal) :=
+  ↑(∏ a in s, f a) = ((∏ a in s, f a) : ennreal) :=
 of_nnreal_hom.map_prod f s
 
 section order

src/data/support.lean

@@ -15,6 +15,7 @@ In this file we define `function.support f = {x | f x ≠ 0}` and prove its basi
 universes u v w x y
 
 open set
+open_locale big_operators
 namespace function
 
 variables {α : Type u} {β : Type v} {ι : Sort w} {A : Type x} {B : Type y}
@@ -104,7 +105,7 @@ end
 
 -- TODO: Drop `classical` once #2332 is merged
 lemma support_prod [integral_domain A] (s : finset α) (f : α → β → A) :
-  support (λ x, s.prod (λ i, f i x)) = ⋂ i ∈ s, support (f i) :=
+  support (λ x, ∏ i in s, f i x) = ⋂ i ∈ s, support (f i) :=
 set.ext $ λ x, by classical;
   simp only [support, ne.def, finset.prod_eq_zero_iff, mem_set_of_eq, set.mem_Inter, not_exists]
 

src/field_theory/finite.lean

@@ -98,10 +98,10 @@ begin
 end
 
 lemma prod_univ_units_id_eq_neg_one :
-  univ.prod (λ x, x) = (-1 : units K) :=
+  (∏ x : units K, x) = (-1 : units K) :=
 begin
   classical,
-  have : ((@univ (units K) _).erase (-1)).prod (λ x, x) = 1,
+  have : (∏ x in (@univ (units K) _).erase (-1), x) = 1,
   from prod_involution (λ x _, x⁻¹) (by simp)
     (λ a, by simp [units.inv_eq_self_iff] {contextual := tt})
     (λ a, by simp [@inv_eq_iff_inv_eq _ _ a, eq_comm] {contextual := tt})

src/field_theory/mv_polynomial.lean

@@ -13,6 +13,7 @@ noncomputable theory
 open_locale classical
 
 open set linear_map submodule
+open_locale big_operators
 
 namespace mv_polynomial
 universes u v
@@ -109,7 +110,7 @@ variables {α : Type*} {σ : Type*}
 variables [field α] [fintype α] [fintype σ]
 
 def indicator (a : σ → α) : mv_polynomial σ α :=
-finset.univ.prod (λn, 1 - (X n - C (a n))^(fintype.card α - 1))
+∏ n, (1 - (X n - C (a n))^(fintype.card α - 1))
 
 lemma eval_indicator_apply_eq_one (a : σ → α) :
   eval a (indicator a) = 1 :=

src/linear_algebra/nonsingular_inverse.lean

@@ -46,7 +46,7 @@ matrix inverse, cramer, cramer's rule, adjugate
 namespace matrix
 universes u v
 variables {n : Type u} [fintype n] [decidable_eq n] {α : Type v}
-open_locale matrix
+open_locale matrix big_operators
 open equiv equiv.perm finset
 
 
@@ -117,8 +117,8 @@ def cramer_map (i : n) : α := (A.update_column i b).det
 lemma cramer_map_is_linear (i : n) : is_linear_map α (λ b, cramer_map A b i) :=
 begin
   have : Π {f : n → n} {i : n} (x : n → α),
-    finset.prod univ (λ (i' : n), (update_column A i x)ᵀ (f i') i')
-    = finset.prod univ (λ (i' : n), if i' = i then x (f i') else A i' (f i')),
+    (∏ i' : n, (update_column A i x)ᵀ (f i') i')
+    = (∏ i' : n, if i' = i then x (f i') else A i' (f i')),
   { intros, congr, ext i', rw [transpose_val, update_column_val] },
   split,
   { intros x y,
@@ -234,7 +234,7 @@ begin
     rw [update_column_val, update_row_val],
     finish },
   { -- Otherwise, we need to show that there is a `0` somewhere in the product.
-    have : univ.prod (λ (j' : n), update_row A j (λ (i' : n), ite (i = i') 1 0) (σ j') j') = 0,
+    have : (∏ j' : n, update_row A j (λ (i' : n), ite (i = i') 1 0) (σ j') j') = 0,
     { apply prod_eq_zero (mem_univ j),
       rw [update_row_self],
       exact if_neg h },

src/number_theory/quadratic_reciprocity.lean

@@ -28,6 +28,7 @@ The proof of quadratic reciprocity implemented uses Gauss' lemma and Eisenstein'
 -/
 
 open function finset nat finite_field zmod
+open_locale big_operators
 
 namespace zmod
 
@@ -117,9 +118,9 @@ end
 @[simp] lemma wilsons_lemma : (nat.fact (p - 1) : zmod p) = -1 :=
 begin
   refine
-  calc (nat.fact (p - 1) : zmod p) = (Ico 1 (succ (p - 1))).prod (λ (x : ℕ), x) :
+  calc (nat.fact (p - 1) : zmod p) = (∏ x in Ico 1 (succ (p - 1)), x) :
     by rw [← finset.prod_Ico_id_eq_fact, prod_nat_cast]
-                               ... = finset.univ.prod (λ x : units (zmod p), x) : _
+                               ... = (∏ x : units (zmod p), x) : _
                                ... = -1 :
     by rw [prod_hom _ (coe : units (zmod p) → zmod p),
            prod_univ_units_id_eq_neg_one, units.coe_neg, units.coe_one],
@@ -142,7 +143,7 @@ begin
     { simp only [val_cast_of_lt hb.right, units.coe_mk0], } }
 end
 
-@[simp] lemma prod_Ico_one_prime : (Ico 1 p).prod (λ x, (x : zmod p)) = -1 :=
+@[simp] lemma prod_Ico_one_prime : (∏ x in Ico 1 p, (x : zmod p)) = -1 :=
 begin
   conv in (Ico 1 p) { rw [← succ_sub_one p, succ_sub (nat.prime.pos ‹p.prime›)] },
   rw [← prod_nat_cast, finset.prod_Ico_id_eq_fact, wilsons_lemma]
@@ -195,24 +196,24 @@ private lemma gauss_lemma_aux₁ (p : ℕ) [hp : fact p.prime] [hp2 : fact (p %
   (-1)^((Ico 1 (p / 2).succ).filter
     (λ x : ℕ, ¬(a * x : zmod p).val ≤ p / 2)).card * (p / 2).fact :=
 calc (a ^ (p / 2) * (p / 2).fact : zmod p) =
-    (Ico 1 (p / 2).succ).prod (λ x, a * x) :
+    (∏ x in Ico 1 (p / 2).succ, a * x) :
   by rw [prod_mul_distrib, ← prod_nat_cast, ← prod_nat_cast, prod_Ico_id_eq_fact,
       prod_const, Ico.card, succ_sub_one]; simp
-... = (Ico 1 (p / 2).succ).prod (λ x, (a * x : zmod p).val) : by simp
-... = (Ico 1 (p / 2).succ).prod
-    (λ x, (if (a * x : zmod p).val ≤ p / 2 then 1 else -1) *
+... = (∏ x in Ico 1 (p / 2).succ, (a * x : zmod p).val) : by simp
+... = (∏ x in Ico 1 (p / 2).succ,
+    (if (a * x : zmod p).val ≤ p / 2 then 1 else -1) *
       (a * x : zmod p).val_min_abs.nat_abs) :
   prod_congr rfl $ λ _ _, begin
     simp only [cast_nat_abs_val_min_abs],
     split_ifs; simp
   end
 ... = (-1)^((Ico 1 (p / 2).succ).filter
       (λ x : ℕ, ¬(a * x : zmod p).val ≤ p / 2)).card *
-    (Ico 1 (p / 2).succ).prod (λ x, (a * x : zmod p).val_min_abs.nat_abs) :
-  have (Ico 1 (p / 2).succ).prod
-        (λ x, if (a * x : zmod p).val ≤ p / 2 then (1 : zmod p) else -1) =
-      ((Ico 1 (p / 2).succ).filter
-        (λ x : ℕ, ¬(a * x : zmod p).val ≤ p / 2)).prod (λ _, -1),
+    (∏ x in Ico 1 (p / 2).succ, (a * x : zmod p).val_min_abs.nat_abs) :
+  have (∏ x in Ico 1 (p / 2).succ,
+        if (a * x : zmod p).val ≤ p / 2 then (1 : zmod p) else -1) =
+      (∏ x in (Ico 1 (p / 2).succ).filter
+        (λ x : ℕ, ¬(a * x : zmod p).val ≤ p / 2), -1),
     from prod_bij_ne_one (λ x _ _, x)
       (λ x, by split_ifs; simp * at * {contextual := tt})
       (λ _ _ _ _ _ _, id)