refactor(data/fintype/basic): split file (#17578)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-import data.fintype.basic
+import data.fintype.powerset
 
 /-!
 # Erdős–Szekeres theorem

archive/imo/imo1987_q1.lean

@@ -3,7 +3,9 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import data.fintype.card
+import data.fintype.big_operators
+import data.fintype.perm
+import data.fintype.prod
 import dynamics.fixed_points.basic
 
 /-!

archive/imo/imo1994_q1.lean

@@ -5,7 +5,7 @@ Authors: Antoine Labelle
 -/
 import algebra.big_operators.basic
 import algebra.big_operators.order
-import data.fintype.card
+import data.fintype.big_operators
 import data.finset.sort
 import data.fin.interval
 import tactic.linarith

src/algebra/big_operators/basic.lean

@@ -7,9 +7,11 @@ Authors: Johannes Hölzl
 import algebra.group.pi
 import algebra.hom.equiv.basic
 import algebra.ring.opposite
-import data.finset.fold
-import data.fintype.basic
 import data.set.pairwise
+import data.finset.sum
+import data.fintype.basic
+import data.finset.sigma
+import algebra.group_power.lemmas
 
 /-!
 # Big operators
@@ -1414,7 +1416,13 @@ end
 @[simp]
 lemma sum_boole {s : finset α} {p : α → Prop} [non_assoc_semiring β] {hp : decidable_pred p} :
   (∑ x in s, if p x then (1 : β) else (0 : β)) = (s.filter p).card :=
-by simp [sum_ite]
+by simp only [add_zero,
+ mul_one,
+ finset.sum_const,
+ nsmul_eq_mul,
+ eq_self_iff_true,
+ finset.sum_const_zero,
+ finset.sum_ite]
 
 lemma _root_.commute.sum_right [non_unital_non_assoc_semiring β] (s : finset α)
   (f : α → β) (b : β) (h : ∀ i ∈ s, commute b (f i)) :

src/algebra/big_operators/fin.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov, Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Anne Baanen
 -/
-import data.fintype.card
+import data.fintype.big_operators
 import data.fintype.fin
 import logic.equiv.fin
 

src/algebra/big_operators/pi.lean

@@ -3,6 +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, Patrick Massot
 -/
+import data.fintype.card
+import algebra.group.prod
 import algebra.big_operators.basic
 import algebra.ring.pi
 

src/algebra/char_zero.lean

@@ -5,7 +5,8 @@ Authors: Mario Carneiro
 -/
 
 import data.nat.cast.field
-import data.fintype.basic
+import data.fintype.lattice
+import algebra.group_power.lemmas
 
 /-!
 # Characteristic zero (additional theorems)

src/algebra/group/conj.lean

@@ -8,6 +8,7 @@ import algebra.group_with_zero.basic
 import algebra.hom.aut
 import algebra.hom.group
 import data.finite.basic
+import data.fintype.units
 
 /-!
 # Conjugacy of group elements

src/algebra/order/field/pi.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import algebra.order.field.basic
-import data.fintype.basic
+import data.fintype.lattice
 
 /-!
 # Lemmas about (finite domain) functions into fields.

src/algebra/order/field/power.lean

@@ -3,6 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
+import algebra.parity
 import algebra.char_zero
 import algebra.group_with_zero.power
 import algebra.order.field.basic