chore(data/list/big_operators): split (#17702)

Split `data.list.big_operators` into `.basic` and `.lemmas`, with the former containing no algebra or set imports.  This should make more of the `fintype` dependency tree portable sooner.

src/algebra/big_operators/multiset.lean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.list.big_operators
+import data.list.big_operators.lemmas
 import data.multiset.basic
 
 /-!

src/algebra/free_monoid/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yury Kudryashov
 -/
-import data.list.big_operators
+import data.list.big_operators.basic
 
 /-!
 # Free monoid over a given alphabet

src/algebra/graded_monoid.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import algebra.group.inj_surj
-import data.list.big_operators
+import data.list.big_operators.basic
 import data.list.range
 import group_theory.group_action.defs
 import group_theory.submonoid.basic

src/control/fold.lean

@@ -3,8 +3,8 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Sean Leather
 -/
+import algebra.group.opposite
 import algebra.free_monoid.basic
-import algebra.opposites
 import control.traversable.instances
 import control.traversable.lemmas
 import category_theory.endomorphism

src/data/list/big_operators.lean → src/data/list/big_operators/basic.lean

@@ -4,17 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 import data.list.forall2
-import algebra.group.opposite
-import algebra.group_power.basic
-import algebra.group_with_zero.commute
-import algebra.group_with_zero.divisibility
-import algebra.order.with_zero
-import algebra.ring.basic
-import algebra.ring.divisibility
-import algebra.ring.commute
-import data.int.basic
-import data.int.units
-import data.set.basic
 
 /-!
 # Sums and products from lists
@@ -138,7 +127,7 @@ end
 @[simp, to_additive]
 lemma prod_take_mul_prod_drop :
   ∀ (L : list M) (i : ℕ), (L.take i).prod * (L.drop i).prod = L.prod
-| [] i := by simp [@zero_le' ℕ]
+| [] i := by simp [nat.zero_le]
 | L 0 := by simp
 | (h :: t) (n+1) := by { dsimp, rw [prod_cons, prod_cons, mul_assoc, prod_take_mul_prod_drop] }
 
@@ -172,7 +161,7 @@ lemma prod_update_nth : ∀ (L : list M) (n : ℕ) (a : M),
     (L.take n).prod * (if n < L.length then a else 1) * (L.drop (n + 1)).prod
 | (x :: xs) 0     a := by simp [update_nth]
 | (x :: xs) (i+1) a := by simp [update_nth, prod_update_nth xs i a, mul_assoc]
-| []      _     _ := by simp [update_nth, (nat.zero_le _).not_lt, @zero_le' ℕ]
+| []      _     _ := by simp [update_nth, (nat.zero_le _).not_lt, nat.zero_le]
 
 open mul_opposite
 
@@ -210,21 +199,6 @@ lemma _root_.commute.list_prod_left (l : list M) (y : M) (h : ∀ (x ∈ l), com
   commute l.prod y  :=
 (commute.list_prod_right _ _ $ λ x hx, (h _ hx).symm).symm
 
-lemma _root_.commute.list_sum_right [non_unital_non_assoc_semiring R] (a : R) (l : list R)
-  (h : ∀ b ∈ l, commute a b) :
-  commute a l.sum :=
-begin
-  induction l with x xs ih,
-  { exact commute.zero_right _, },
-  { rw sum_cons,
-    exact (h _ $ mem_cons_self _ _).add_right (ih $ λ j hj, h _ $ mem_cons_of_mem _ hj) }
-end
-
-lemma _root_.commute.list_sum_left [non_unital_non_assoc_semiring R] (b : R) (l : list R)
-  (h : ∀ a ∈ l, commute a b) :
-  commute l.sum b :=
-(commute.list_sum_right _ _ $ λ x hx, (h _ hx).symm).symm
-
 @[to_additive sum_le_sum] lemma forall₂.prod_le_prod' [preorder M]
   [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
   {l₁ l₂ : list M} (h : forall₂ (≤) l₁ l₂) : l₁.prod ≤ l₂.prod :=
@@ -293,13 +267,6 @@ lemma prod_le_pow_card [preorder M]
   l.prod ≤ n ^ l.length :=
 by simpa only [map_id'', map_const, prod_repeat] using prod_le_prod' h
 
-@[to_additive card_nsmul_le_sum]
-lemma pow_card_le_prod [preorder M]
-  [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
-  (l : list M) (n : M) (h : ∀ (x ∈ l), n ≤ x) :
-  n ^ l.length ≤ l.prod :=
-@prod_le_pow_card Mᵒᵈ _ _ _ _ l n h
-
 @[to_additive exists_lt_of_sum_lt] lemma exists_lt_of_prod_lt' [linear_order M]
   [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)] {l : list ι}
   (f g : ι → M) (h : (l.map f).prod < (l.map g).prod) :
@@ -461,39 +428,21 @@ lemma all_one_of_le_one_le_of_prod_eq_one [ordered_comm_monoid M]
   x = 1 :=
 le_antisymm (hl₂ ▸ single_le_prod hl₁ _ hx) (hl₁ x hx)
 
-@[to_additive] lemma prod_eq_one_iff [canonically_ordered_monoid M] (l : list M) :
-  l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M) :=
-⟨all_one_of_le_one_le_of_prod_eq_one (λ _ _, one_le _),
-  λ h, by rw [eq_repeat.2 ⟨rfl, h⟩, prod_repeat, one_pow]⟩
-
 /-- Slightly more general version of `list.prod_eq_one_iff` for a non-ordered `monoid` -/
 @[to_additive "Slightly more general version of `list.sum_eq_zero_iff`
   for a non-ordered `add_monoid`"]
 lemma prod_eq_one [monoid M] {l : list M} (hl : ∀ (x ∈ l), x = (1 : M)) : l.prod = 1 :=
-trans (prod_eq_pow_card l 1 hl) (one_pow l.length)
+begin
+  induction l with i l hil,
+  { refl },
+  rw [list.prod_cons, hil (λ x hx, hl _ (mem_cons_of_mem i hx)), hl _ (mem_cons_self i l), one_mul]
+end
 
 @[to_additive]
 lemma exists_mem_ne_one_of_prod_ne_one [monoid M] {l : list M} (h : l.prod ≠ 1) :
   ∃ (x ∈ l), x ≠ (1 : M) :=
 by simpa only [not_forall] using mt prod_eq_one h
 
-/-- If a product of integers is `-1`, then at least one factor must be `-1`. -/
-lemma neg_one_mem_of_prod_eq_neg_one {l : list ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l :=
-begin
-  obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h dec_trivial),
-  exact or.resolve_left (int.is_unit_iff.mp (prod_is_unit_iff.mp
-         (h.symm ▸ is_unit.neg is_unit_one : is_unit l.prod) x h₁)) h₂ ▸ h₁,
-end
-
-/-- If all elements in a list are bounded below by `1`, then the length of the list is bounded
-by the sum of the elements. -/
-lemma length_le_sum_of_one_le (L : list ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum :=
-begin
-  induction L with j L IH h, { simp },
-  rw [sum_cons, length, add_comm],
-  exact add_le_add (h _ (set.mem_insert _ _)) (IH (λ i hi, h i (set.mem_union_right _ hi)))
-end
-
 -- TODO: develop theory of tropical rings
 lemma sum_le_foldr_max [add_monoid M] [add_monoid N] [linear_order N] (f : M → N)
   (h0 : f 0 ≤ 0) (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : list M) :
@@ -526,21 +475,9 @@ lemma prod_map_erase [decidable_eq ι] [comm_monoid M] (f : ι → M) {a} :
         mul_left_comm (f a) (f b)], }
   end
 
-lemma dvd_prod [comm_monoid M] {a} {l : list M} (ha : a ∈ l) : a ∣ l.prod :=
-let ⟨s, t, h⟩ := mem_split ha in
-by { rw [h, prod_append, prod_cons, mul_left_comm], exact dvd_mul_right _ _ }
-
 @[simp] lemma sum_const_nat (m n : ℕ) : sum (list.repeat m n) = m * n :=
 by induction n; [refl, simp only [*, repeat_succ, sum_cons, nat.mul_succ, add_comm]]
 
-lemma dvd_sum [semiring R] {a} {l : list R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum :=
-begin
-  induction l with x l ih,
-  { exact dvd_zero _ },
-  { rw [list.sum_cons],
-    exact dvd_add (h _ (mem_cons_self _ _)) (ih (λ x hx, h x (mem_cons_of_mem _ hx))) }
-end
-
 /-- The product of a list of positive natural numbers is positive,
 and likewise for any nontrivial ordered semiring. -/
 lemma prod_pos [strict_ordered_semiring R] (l : list R) (h : ∀ a ∈ l, (0 : R) < a) : 0 < l.prod :=
@@ -596,54 +533,10 @@ by rw [alternating_prod_cons_cons', alternating_prod_cons' b l, mul_inv, inv_inv
   alternating_prod (a :: l) = a / alternating_prod l :=
 by rw [div_eq_mul_inv, alternating_prod_cons']
 
-@[to_additive]
-lemma alternating_prod_append : ∀ l₁ l₂ : list α,
-  alternating_prod (l₁ ++ l₂) = alternating_prod l₁ * alternating_prod l₂ ^ (-1 : ℤ) ^ length l₁
-| [] l₂ := by simp
-| (a :: l₁) l₂ := by simp_rw [cons_append, alternating_prod_cons, alternating_prod_append,
-  length_cons, pow_succ, neg_mul, one_mul, zpow_neg, ←div_eq_mul_inv, div_div]
-
-@[to_additive]
-lemma alternating_prod_reverse :
-  ∀ l : list α, alternating_prod (reverse l) = alternating_prod l ^ (-1 : ℤ) ^ (length l + 1)
-| [] := by simp only [alternating_prod_nil, one_zpow, reverse_nil]
-| (a :: l) :=
-begin
-  simp_rw [reverse_cons, alternating_prod_append, alternating_prod_reverse,
-    alternating_prod_singleton, alternating_prod_cons, length_reverse, length, pow_succ, neg_mul,
-    one_mul, zpow_neg, inv_inv],
-  rw [mul_comm, ←div_eq_mul_inv, div_zpow],
-end
-
 end alternating
 
-lemma sum_map_mul_left [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
-  (L.map (λ b, r * f b)).sum = r * (L.map f).sum :=
-sum_map_hom L f $ add_monoid_hom.mul_left r
-
-lemma sum_map_mul_right [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
-  (L.map (λ b, f b * r)).sum = (L.map f).sum * r :=
-sum_map_hom L f $ add_monoid_hom.mul_right r
-
 end list
 
-namespace mul_opposite
-
-open list
-variables [monoid M]
-
-lemma op_list_prod : ∀ (l : list M), op (l.prod) = (l.map op).reverse.prod
-| [] := rfl
-| (x :: xs) := by rw [list.prod_cons, list.map_cons, list.reverse_cons', list.prod_concat, op_mul,
-                      op_list_prod]
-
-lemma _root_.mul_opposite.unop_list_prod (l : list Mᵐᵒᵖ) :
-  (l.prod).unop = (l.map unop).reverse.prod :=
-by rw [← op_inj, op_unop, mul_opposite.op_list_prod, map_reverse, map_map, reverse_reverse,
-  op_comp_unop, map_id]
-
-end mul_opposite
-
 section monoid_hom
 
 variables [monoid M] [monoid N]
@@ -653,11 +546,6 @@ lemma map_list_prod {F : Type*} [monoid_hom_class F M N] (f : F)
   (l : list M) : f l.prod = (l.map f).prod :=
 (l.prod_hom f).symm
 
-/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements. -/
-lemma unop_map_list_prod {F : Type*} [monoid_hom_class F M Nᵐᵒᵖ] (f : F) (l : list M) :
-  (f l.prod).unop = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
-by rw [map_list_prod f l, mul_opposite.unop_list_prod, list.map_map]
-
 namespace monoid_hom
 
 /-- Deprecated, use `_root_.map_list_prod` instead. -/
@@ -666,13 +554,6 @@ protected lemma map_list_prod (f : M →* N) (l : list M) :
   f l.prod = (l.map f).prod :=
 map_list_prod f l
 
-/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements.
-
-Deprecated, use `_root_.unop_map_list_prod` instead. -/
-protected lemma unop_map_list_prod (f : M →* Nᵐᵒᵖ) (l : list M) :
-  (f l.prod).unop = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
-unop_map_list_prod f l
-
 end monoid_hom
 
 end monoid_hom