chore(data/rat/cast): split (#17761)

Split off `data/rat/big_operators` from `data/rat/cast`, removing the `algebra/big_operators/basic` import (and, as a consequence, `finset`) from the latter.



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Author: hrmacbeth

src/algebra/module/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
+import algebra.big_operators.basic
 import algebra.smul_with_zero
 import group_theory.group_action.group
 import tactic.abel

src/data/bitvec/basic.lean

@@ -5,6 +5,7 @@ Authors: Simon Hudon
 -/
 import data.bitvec.core
 import data.fin.basic
+import tactic.monotonicity
 import tactic.norm_num
 
 namespace bitvec

src/data/finset/sym.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import data.finset.lattice
 import data.fintype.prod
 import data.fintype.vector
 import data.sym.sym2

src/data/finsupp/basic.lean

@@ -8,6 +8,7 @@ import algebra.hom.group_action
 import algebra.regular.smul
 import data.finset.preimage
 import data.list.alist
+import data.rat.big_operators
 
 /-!
 # Miscellaneous definitions, lemmas, and constructions using finsupp

src/data/rat/big_operators.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2019 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import data.rat.cast
+import algebra.big_operators.basic
+
+/-! # Casting lemmas for rational numbers involving sums and products
+-/
+
+open_locale big_operators
+
+variables {ι α : Type*}
+
+namespace rat
+
+section with_div_ring
+variables [division_ring α] [char_zero α]
+
+@[simp, norm_cast] lemma cast_list_sum (s : list ℚ) : (↑(s.sum) : α) = (s.map coe).sum :=
+map_list_sum (rat.cast_hom α) _
+
+@[simp, norm_cast] lemma cast_multiset_sum (s : multiset ℚ) : (↑(s.sum) : α) = (s.map coe).sum :=
+map_multiset_sum (rat.cast_hom α) _
+
+@[simp, norm_cast] lemma cast_sum (s : finset ι) (f : ι → ℚ) :
+  (↑(∑ i in s, f i) : α) = ∑ i in s, f i :=
+map_sum (rat.cast_hom α) _ _
+
+@[simp, norm_cast] lemma cast_list_prod (s : list ℚ) : (↑(s.prod) : α) = (s.map coe).prod :=
+map_list_prod (rat.cast_hom α) _
+
+end with_div_ring
+
+section field
+variables [field α] [char_zero α]
+
+@[simp, norm_cast] lemma cast_multiset_prod (s : multiset ℚ) : (↑(s.prod) : α) = (s.map coe).prod :=
+map_multiset_prod (rat.cast_hom α) _
+
+@[simp, norm_cast] lemma cast_prod (s : finset ι) (f : ι → ℚ) :
+  (↑(∏ i in s, f i) : α) = ∏ i in s, f i :=
+map_prod (rat.cast_hom α) _ _
+
+end field
+
+end rat

src/data/rat/cast.lean

@@ -9,7 +9,6 @@ import data.int.char_zero
 import algebra.group_with_zero.power
 import algebra.field.opposite
 import algebra.order.field.basic
-import algebra.big_operators.basic
 
 /-!
 # Casts for Rational Numbers
@@ -28,8 +27,6 @@ casting lemmas showing the well-behavedness of this injection.
 rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting
 -/
 
-open_locale big_operators
-
 variables {F ι α β : Type*}
 
 namespace rat
@@ -211,33 +208,8 @@ by simp only [mk_eq_div, cast_div, cast_coe_int]
 @[simp, norm_cast] theorem cast_pow (q) (k : ℕ) : ((q ^ k : ℚ) : α) = q ^ k :=
 (cast_hom α).map_pow q k
 
-@[simp, norm_cast] lemma cast_list_sum (s : list ℚ) : (↑(s.sum) : α) = (s.map coe).sum :=
-map_list_sum (rat.cast_hom α) _
-
-@[simp, norm_cast] lemma cast_multiset_sum (s : multiset ℚ) : (↑(s.sum) : α) = (s.map coe).sum :=
-map_multiset_sum (rat.cast_hom α) _
-
-@[simp, norm_cast] lemma cast_sum (s : finset ι) (f : ι → ℚ) :
-  (↑(∑ i in s, f i) : α) = ∑ i in s, f i :=
-map_sum (rat.cast_hom α) _ _
-
-@[simp, norm_cast] lemma cast_list_prod (s : list ℚ) : (↑(s.prod) : α) = (s.map coe).prod :=
-map_list_prod (rat.cast_hom α) _
-
 end with_div_ring
 
-section field
-variables [field α] [char_zero α]
-
-@[simp, norm_cast] lemma cast_multiset_prod (s : multiset ℚ) : (↑(s.prod) : α) = (s.map coe).prod :=
-map_multiset_prod (rat.cast_hom α) _
-
-@[simp, norm_cast] lemma cast_prod (s : finset ι) (f : ι → ℚ) :
-  (↑(∏ i in s, f i) : α) = ∏ i in s, f i :=
-map_prod (rat.cast_hom α) _ _
-
-end field
-
 section linear_ordered_field
 
 variables {K : Type*} [linear_ordered_field K]

src/data/sym/sym2.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Kyle Miller All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
+import data.finset.prod
 import data.sym.basic
 import tactic.linarith
 
@@ -41,7 +42,7 @@ term of the symmetric square.
 symmetric square, unordered pairs, symmetric powers
 -/
 
-open finset fintype function sym
+open finset function sym
 
 universe u
 variables {α β γ : Type*}

src/tactic/norm_fin.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky, Mario Carneiro
 -/
 
+import data.fin.basic
 import tactic.norm_num
 
 /-!

src/tactic/omega/clause.lean

@@ -8,6 +8,7 @@ Authors: Seul Baek
 Definition of linear constrain clauses.
 -/
 
+import data.list.basic
 import tactic.omega.term
 
 namespace omega

src/tactic/ring.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import tactic.norm_num
+import data.fin.basic
 
 /-!
 # `ring`