From be183e26fdcb2bc3315cd7e1429421dc441c6d8d Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Fri, 4 Jun 2021 03:56:15 +0000
Subject: [PATCH] chore(data/finset|multiset|finsupp): reduce algebra/ imports
 (#7797)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
---
 src/algebra/big_operators/basic.lean       |  5 +++++
 src/algebra/big_operators/finsupp.lean     | 17 +++++++++++++++++
 src/algebra/gcd_monoid.lean                |  1 +
 src/algebra/group_power/lemmas.lean        | 16 ----------------
 src/algebra/iterate_hom.lean               |  1 -
 src/algebra/monoid_algebra.lean            |  1 +
 src/data/finsupp/basic.lean                | 14 +-------------
 src/data/finsupp/lattice.lean              |  1 -
 src/data/list/basic.lean                   | 15 ++++++++++++++-
 src/data/list/indexes.lean                 | 12 +++++++-----
 src/data/list/perm.lean                    |  1 -
 src/data/multiset/basic.lean               | 19 +++++++------------
 src/data/multiset/range.lean               |  2 ++
 src/data/mv_polynomial/variables.lean      |  2 +-
 src/data/nat/basic.lean                    |  3 +++
 src/linear_algebra/linear_independent.lean |  1 +
 src/linear_algebra/multilinear.lean        |  1 +
 17 files changed, 61 insertions(+), 51 deletions(-)

diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
index c1bfa596b4927..f1aca04049f6c 100644
--- a/src/algebra/big_operators/basic.lean
+++ b/src/algebra/big_operators/basic.lean
@@ -1377,6 +1377,11 @@ namespace list
 end list
 
 namespace multiset
+
+lemma abs_sum_le_sum_abs [linear_ordered_add_comm_group α] {s : multiset α} :
+  abs s.sum ≤ (s.map abs).sum :=
+le_sum_of_subadditive _ abs_zero abs_add s
+
 variables [decidable_eq α]
 
 @[simp] lemma to_finset_sum_count_eq (s : multiset α) :
diff --git a/src/algebra/big_operators/finsupp.lean b/src/algebra/big_operators/finsupp.lean
index 38376ff7a9027..bd1230c7ffdab 100644
--- a/src/algebra/big_operators/finsupp.lean
+++ b/src/algebra/big_operators/finsupp.lean
@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 
 import algebra.big_operators.pi
+import algebra.big_operators.ring
 import data.finsupp
 
 /-!
@@ -26,6 +27,7 @@ theorem finset.sum_apply' : (∑ k in s, f k) i = ∑ k in s, f k i :=
 theorem finsupp.sum_apply' : g.sum k x = g.sum (λ i b, k i b x) :=
 finset.sum_apply _ _ _
 
+section
 include h0 h1
 
 open_locale classical
@@ -33,3 +35,18 @@ open_locale classical
 theorem finsupp.sum_sum_index' : (∑ x in s, f x).sum t = ∑ x in s, (f x).sum t :=
 finset.induction_on s rfl $ λ a s has ih,
 by simp_rw [finset.sum_insert has, finsupp.sum_add_index h0 h1, ih]
+
+end
+
+section
+variables {R S : Type*} [semiring R] [semiring S]
+
+lemma finsupp.sum_mul (b : S) (s : α →₀ R) {f : α → R → S} :
+  (s.sum f) * b = s.sum (λ a c, (f a c) * b) :=
+by simp only [finsupp.sum, finset.sum_mul]
+
+lemma finsupp.mul_sum (b : S) (s : α →₀ R) {f : α → R → S} :
+  b * (s.sum f) = s.sum (λ a c, b * (f a c)) :=
+by simp only [finsupp.sum, finset.mul_sum]
+
+end
diff --git a/src/algebra/gcd_monoid.lean b/src/algebra/gcd_monoid.lean
index 1152cf97916e2..7fe3510ae3f25 100644
--- a/src/algebra/gcd_monoid.lean
+++ b/src/algebra/gcd_monoid.lean
@@ -9,6 +9,7 @@ TODO: Generalize GCD monoid to not require normalization in all cases
 -/
 import algebra.associated
 import data.nat.gcd
+import algebra.group_power.lemmas
 
 /-!
 
diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean
index 34d7bfe326083..7ef69ec6cf087 100644
--- a/src/algebra/group_power/lemmas.lean
+++ b/src/algebra/group_power/lemmas.lean
@@ -35,18 +35,6 @@ add_monoid_hom.eq_nat_cast
   ⟨λ n, n • (1 : A), zero_nsmul _, λ _ _, add_nsmul _ _ _⟩
   (one_nsmul _)
 
-@[simp, priority 500]
-theorem list.prod_repeat (a : M) (n : ℕ) : (list.repeat a n).prod = a ^ n :=
-begin
-  induction n with n ih,
-  { rw pow_zero, refl },
-  { rw [list.repeat_succ, list.prod_cons, ih, pow_succ] }
-end
-
-@[simp, priority 500]
-theorem list.sum_repeat : ∀ (a : A) (n : ℕ), (list.repeat a n).sum = n • a :=
-@list.prod_repeat (multiplicative A) _
-
 @[simp, norm_cast] lemma units.coe_pow (u : units M) (n : ℕ) : ((u ^ n : units M) : M) = u ^ n :=
 (units.coe_hom M).map_pow u n
 
@@ -85,10 +73,6 @@ end
 
 end monoid
 
-theorem nat.nsmul_eq_mul (m n : ℕ) : m • n = m * n :=
-by induction m with m ih; [rw [zero_nsmul, zero_mul],
-  rw [succ_nsmul', ih, nat.succ_mul]]
-
 section group
 variables [group G] [group H] [add_group A] [add_group B]
 
diff --git a/src/algebra/iterate_hom.lean b/src/algebra/iterate_hom.lean
index add349ecc0600..4e39f04e99897 100644
--- a/src/algebra/iterate_hom.lean
+++ b/src/algebra/iterate_hom.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 
-import algebra.group_power
 import algebra.group_power.basic
 import logic.function.iterate
 import group_theory.perm.basic
diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean
index 3c92c0b7b2bd9..58bf4192542d6 100644
--- a/src/algebra/monoid_algebra.lean
+++ b/src/algebra/monoid_algebra.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury G. Kudryashov, Scott Morrison
 -/
 import algebra.algebra.basic
+import algebra.big_operators.finsupp
 import linear_algebra.finsupp
 
 /-!
diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean
index e350b0227b4ea..56635842ec6ff 100644
--- a/src/data/finsupp/basic.lean
+++ b/src/data/finsupp/basic.lean
@@ -3,10 +3,6 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Scott Morrison
 -/
-import algebra.big_operators.order
-import algebra.module.pi
-import group_theory.submonoid.basic
-import algebra.big_operators.ring
 import data.finset.preimage
 import algebra.indicator_function
 
@@ -2104,15 +2100,7 @@ instance [semiring R] [add_comm_monoid M] [module R M] {ι : Type*}
   (λ i, (smul_eq_zero.mp (finsupp.ext_iff.mp h i)).resolve_left hc))⟩
 
 section
-variables [semiring R] [semiring S]
-
-lemma sum_mul (b : S) (s : α →₀ R) {f : α → R → S} :
-  (s.sum f) * b = s.sum (λ a c, (f a c) * b) :=
-by simp only [finsupp.sum, finset.sum_mul]
-
-lemma mul_sum (b : S) (s : α →₀ R) {f : α → R → S} :
-  b * (s.sum f) = s.sum (λ a c, b * (f a c)) :=
-by simp only [finsupp.sum, finset.mul_sum]
+variables [has_zero R]
 
 instance unique_of_right [subsingleton R] : unique (α →₀ R) :=
 { uniq := λ l, ext $ λ i, subsingleton.elim _ _,
diff --git a/src/data/finsupp/lattice.lean b/src/data/finsupp/lattice.lean
index fe6beb9bea6fe..536bb9a1da5b9 100644
--- a/src/data/finsupp/lattice.lean
+++ b/src/data/finsupp/lattice.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import data.finsupp.basic
-import algebra.ordered_group
 
 /-!
 # Lattice structure on finsupps
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index 416d9f1cdd1cc..34396e367320d 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -3,10 +3,10 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
-import algebra.order_functions
 import control.monad.basic
 import data.nat.basic
 import order.rel_classes
+import algebra.group_power.basic
 
 /-!
 # Basic properties of lists
@@ -2250,6 +2250,19 @@ theorem prod_cons : (a::l).prod = a * l.prod :=
 calc (a::l).prod = foldl (*) (a * 1) l : by simp only [list.prod, foldl_cons, one_mul, mul_one]
   ... = _ : foldl_assoc
 
+@[simp, priority 500]
+theorem prod_repeat (a : α) (n : ℕ) : (list.repeat a n).prod = a ^ n :=
+begin
+  induction n with n ih,
+  { rw pow_zero, refl },
+  { rw [list.repeat_succ, list.prod_cons, ih, pow_succ] }
+end
+
+@[simp, priority 500]
+theorem sum_repeat {α : Type*} [add_monoid α] :
+  ∀ (a : α) (n : ℕ), (list.repeat a n).sum = n • a :=
+@list.prod_repeat (multiplicative α) _
+
 @[simp, to_additive]
 theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod :=
 calc (l₁ ++ l₂).prod = foldl (*) (foldl (*) 1 l₁ * 1) l₂ : by simp [list.prod]
diff --git a/src/data/list/indexes.lean b/src/data/list/indexes.lean
index 5d5976fe41350..04cc869a348ca 100644
--- a/src/data/list/indexes.lean
+++ b/src/data/list/indexes.lean
@@ -3,12 +3,14 @@ Copyright (c) 2020 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
-import data.list.basic
-import data.list.defs
-import data.list.zip
 import data.list.range
-import logic.basic
+
+/-! 
+# Lemmas about list.*_with_index functions.
+
+Some specification lemmas for `list.map_with_index`, `list.mmap_with_index`, `list.foldl_with_index`
+and `list.foldr_with_index`.
+-/
 
 universes u v
 
diff --git a/src/data/list/perm.lean b/src/data/list/perm.lean
index 2aa0280fd3c77..d8987584e9a04 100644
--- a/src/data/list/perm.lean
+++ b/src/data/list/perm.lean
@@ -7,7 +7,6 @@ import data.list.bag_inter
 import data.list.erase_dup
 import data.list.zip
 import logic.relation
-import data.nat.factorial
 
 /-!
 # List permutations
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
index aa0e5ab1edeb9..7c766acbb953f 100644
--- a/src/data/multiset/basic.lean
+++ b/src/data/multiset/basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.list.perm
-import algebra.group_power
 
 /-!
 # Multisets
@@ -833,6 +832,13 @@ prod_eq_foldl _
 
 attribute [norm_cast] coe_prod coe_sum
 
+@[simp, to_additive] theorem prod_to_list [comm_monoid α] (s : multiset α) :
+  s.to_list.prod = s.prod :=
+begin
+  conv_rhs { rw ←coe_to_list s, },
+  rw coe_prod,
+end
+
 @[simp, to_additive]
 theorem prod_zero [comm_monoid α] : @prod α _ 0 = 1 := rfl
 
@@ -1042,10 +1048,6 @@ lemma le_prod_nonempty_of_submultiplicative [comm_monoid α] [ordered_comm_monoi
 le_prod_nonempty_of_submultiplicative_on_pred f (λ i, true) (by simp [h_mul]) (by simp) s
   hs_nonempty (by simp)
 
-lemma abs_sum_le_sum_abs [linear_ordered_field α] {s : multiset α} :
-  abs s.sum ≤ (s.map abs).sum :=
-le_sum_of_subadditive _ abs_zero abs_add s
-
 theorem dvd_sum [comm_semiring α] {a : α} {s : multiset α} : (∀ x ∈ s, a ∣ x) → a ∣ s.sum :=
 multiset.induction_on s (λ _, dvd_zero _)
   (λ x s ih h, by rw sum_cons; exact dvd_add
@@ -1054,13 +1056,6 @@ multiset.induction_on s (λ _, dvd_zero _)
 @[simp] theorem sum_map_singleton (s : multiset α) : (s.map (λ a, a ::ₘ 0)).sum = s :=
 multiset.induction_on s (by simp) (by simp)
 
-@[simp, to_additive] theorem prod_to_list [comm_monoid α] (s : multiset α) :
-  s.to_list.prod = s.prod :=
-begin
-  conv_rhs { rw ←coe_to_list s, },
-  rw coe_prod,
-end
-
 /-! ### Join -/
 
 /-- `join S`, where `S` is a multiset of multisets, is the lift of the list join
diff --git a/src/data/multiset/range.lean b/src/data/multiset/range.lean
index 65dfa8ef19bc8..e6dc92578e4b4 100644
--- a/src/data/multiset/range.lean
+++ b/src/data/multiset/range.lean
@@ -6,6 +6,8 @@ Authors: Mario Carneiro
 import data.multiset.basic
 import data.list.range
 
+/-! # `multiset.range n` gives `{0, 1, ..., n-1}` as a multiset. -/
+
 open list nat
 
 namespace multiset
diff --git a/src/data/mv_polynomial/variables.lean b/src/data/mv_polynomial/variables.lean
index 495b04d227efc..d9e843b72a1c8 100644
--- a/src/data/mv_polynomial/variables.lean
+++ b/src/data/mv_polynomial/variables.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
-
+import algebra.big_operators.order
 import data.mv_polynomial.monad
 import data.set.disjointed
 
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
index c65cab974d7d3..9dd6bdcfd01ac 100644
--- a/src/data/nat/basic.lean
+++ b/src/data/nat/basic.lean
@@ -105,6 +105,9 @@ instance nat.subtype.semilattice_sup_bot (s : set ℕ) [decidable_pred s] [h : n
   ..subtype.linear_order s,
   ..lattice_of_linear_order }
 
+theorem nat.nsmul_eq_mul (m n : ℕ) : m • n = m * n :=
+rfl
+
 theorem nat.eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : 0 < m) (H : n * m = k * m) : n = k :=
 by rw [mul_comm n m, mul_comm k m] at H; exact nat.eq_of_mul_eq_mul_left Hm H
 
diff --git a/src/linear_algebra/linear_independent.lean b/src/linear_algebra/linear_independent.lean
index 13a71c0721cd3..7e0eae7b90a75 100644
--- a/src/linear_algebra/linear_independent.lean
+++ b/src/linear_algebra/linear_independent.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp, Anne Baanen
 -/
+import algebra.big_operators.finsupp
 import linear_algebra.finsupp
 import linear_algebra.prod
 import linear_algebra.pi
diff --git a/src/linear_algebra/multilinear.lean b/src/linear_algebra/multilinear.lean
index 3dd91ca4a43aa..52658d431157a 100644
--- a/src/linear_algebra/multilinear.lean
+++ b/src/linear_algebra/multilinear.lean
@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import linear_algebra.basic
 import algebra.algebra.basic
+import algebra.big_operators.order
 import data.fintype.sort
 
 /-!