chore(data/fintype): move results depending on big_operators (#2044)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: kim-em

src/algebra/big_operators.lean

@@ -5,8 +5,7 @@ Authors: Johannes Hölzl
 
 Some big operators for lists and finite sets.
 -/
-import tactic.tauto data.list.basic data.finset data.nat.enat
-import algebra.group algebra.ordered_group algebra.group_power
+import tactic.tauto data.list.defs data.finset data.nat.enat
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}

src/analysis/normed_space/multilinear.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 
 import analysis.normed_space.operator_norm topology.algebra.multilinear
+import data.fintype.card
 
 /-!
 # Operator norm on the space of continuous multilinear maps

src/data/fintype.lean

@@ -5,7 +5,7 @@ Author: Mario Carneiro
 
 Finite types.
 -/
-import data.finset algebra.big_operators data.array.lemmas logic.unique
+import data.finset data.array.lemmas logic.unique
 import tactic.wlog
 universes u v
 
@@ -196,9 +196,6 @@ def of_subsingleton (a : α) [subsingleton α] : fintype α :=
 @[simp] theorem card_of_subsingleton (a : α) [subsingleton α] :
   @fintype.card _ (of_subsingleton a) = 1 := rfl
 
-lemma card_eq_sum_ones {α} [fintype α] : fintype.card α = (finset.univ : finset α).sum (λ _, 1) :=
-finset.card_eq_sum_ones _
-
 end fintype
 
 namespace set
@@ -237,22 +234,6 @@ begin
   exact fin.cases (or.inl rfl) (λ i, or.inr ⟨i, trivial, rfl⟩) m
 end
 
-theorem fin.prod_univ_succ [comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
-  univ.prod f = f 0 * univ.prod (λ i:fin n, f i.succ) :=
-begin
-  rw [fin.univ_succ, prod_insert, prod_image],
-  { intros x _ y _ hxy, exact fin.succ.inj hxy },
-  { simpa using fin.succ_ne_zero }
-end
-
-@[simp, to_additive] theorem fin.prod_univ_zero [comm_monoid β] (f : fin 0 → β) : univ.prod f = 1 := rfl
-
-theorem fin.sum_univ_succ [add_comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
-  univ.sum f = f 0 + univ.sum (λ i:fin n, f i.succ) :=
-by apply @fin.prod_univ_succ (multiplicative β)
-
-attribute [to_additive] fin.prod_univ_succ
-
 lemma fin.univ_cast_succ (n : ℕ) :
   (univ : finset (fin $ n+1)) = insert (fin.last n) (univ.image fin.cast_succ) :=
 begin
@@ -266,19 +247,6 @@ begin
     exact fin.eq_last_of_not_lt h }
 end
 
-theorem fin.prod_univ_cast_succ [comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
-  univ.prod f = univ.prod (λ i:fin n, f i.cast_succ) * f (fin.last n) :=
-begin
-  rw [fin.univ_cast_succ, prod_insert, prod_image, mul_comm],
-  { intros x _ y _ hxy, exact fin.cast_succ_inj.mp hxy },
-  { simpa using fin.cast_succ_ne_last }
-end
-
-theorem fin.sum_univ_cast_succ [add_comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
-  univ.sum f = univ.sum (λ i:fin n, f i.cast_succ) + f (fin.last n) :=
-by apply @fin.prod_univ_cast_succ (multiplicative β)
-attribute [to_additive] fin.prod_univ_cast_succ
-
 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 ⟨finset.singleton (default α), λ x, by rw [unique.eq_default x]; simp⟩
 
@@ -347,11 +315,6 @@ instance {α : Type*} (β : α → Type*)
   [fintype α] [∀ a, fintype (β a)] : fintype (sigma β) :=
 ⟨univ.sigma (λ _, univ), λ ⟨a, b⟩, by simp⟩
 
-@[simp] theorem fintype.card_sigma {α : Type*} (β : α → Type*)
-  [fintype α] [∀ a, fintype (β a)] :
-  fintype.card (sigma β) = univ.sum (λ a, fintype.card (β a)) :=
-card_sigma _ _
-
 instance (α β : Type*) [fintype α] [fintype β] : fintype (α × β) :=
 ⟨univ.product univ, λ ⟨a, b⟩, by simp⟩
 
@@ -381,10 +344,6 @@ instance (α : Type u) (β : Type v) [fintype α] [fintype β] : fintype (α ⊕
   ((equiv.sum_equiv_sigma_bool _ _).symm.trans
     (equiv.sum_congr equiv.ulift equiv.ulift))
 
-@[simp] theorem fintype.card_sum (α β : Type*) [fintype α] [fintype β] :
-  fintype.card (α ⊕ β) = fintype.card α + fintype.card β :=
-by rw [sum.fintype, fintype.of_equiv_card]; simp
-
 lemma fintype.card_le_of_injective [fintype α] [fintype β] (f : α → β)
   (hf : function.injective f) : fintype.card α ≤ fintype.card β :=
 by haveI := classical.prop_decidable; exact
@@ -486,18 +445,6 @@ instance pi.fintype {α : Type*} {β : α → Type*}
     λ f, finset.mem_pi.2 $ λ a ha, mem_univ _⟩
   ⟨λ f a, f a (mem_univ _), λ f a _, f a, λ f, rfl, λ f, rfl⟩
 
-@[simp] lemma fintype.card_pi {β : α → Type*} [fintype α] [decidable_eq α]
-  [f : Π a, fintype (β a)] : fintype.card (Π a, β a) = univ.prod (λ a, fintype.card (β a)) :=
-by letI f' : fintype (Πa∈univ, β a) :=
-  ⟨(univ.pi $ λa, univ), assume f, finset.mem_pi.2 $ assume a ha, mem_univ _⟩;
-exact calc fintype.card (Π a, β a) = fintype.card (Π a ∈ univ, β a) : fintype.card_congr
-  ⟨λ f a ha, f a, λ f a, f a (mem_univ a), λ _, rfl, λ _, rfl⟩
-... = univ.prod (λ a, fintype.card (β a)) : finset.card_pi _ _
-
-@[simp] lemma fintype.card_fun [fintype α] [decidable_eq α] [fintype β] :
-  fintype.card (α → β) = fintype.card β ^ fintype.card α :=
-by rw [fintype.card_pi, finset.prod_const, nat.pow_eq_pow]; refl
-
 instance d_array.fintype {n : ℕ} {α : fin n → Type*}
   [∀n, fintype (α n)] : fintype (d_array n α) :=
 fintype.of_equiv _ (equiv.d_array_equiv_fin _).symm
@@ -508,10 +455,6 @@ d_array.fintype
 instance vector.fintype {α : Type*} [fintype α] {n : ℕ} : fintype (vector α n) :=
 fintype.of_equiv _ (equiv.vector_equiv_fin _ _).symm
 
-@[simp] lemma card_vector [fintype α] (n : ℕ) :
-  fintype.card (vector α n) = fintype.card α ^ n :=
-by rw fintype.of_equiv_card; simp
-
 instance quotient.fintype [fintype α] (s : setoid α)
   [decidable_rel ((≈) : α → α → Prop)] : fintype (quotient s) :=
 fintype.of_surjective quotient.mk (λ x, quotient.induction_on x (λ x, ⟨x, rfl⟩))
@@ -614,24 +557,6 @@ begin
   simp [this], exact setoid.refl _
 end
 
-@[simp, to_additive]
-lemma finset.prod_attach_univ [fintype α] [comm_monoid β] (f : {a : α // a ∈ @univ α _} → β) :
-  univ.attach.prod (λ x, f x) = univ.prod (λ x, f ⟨x, (mem_univ _)⟩) :=
-prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp) (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩)
-
-@[to_additive]
-lemma finset.range_prod_eq_univ_prod [comm_monoid β] (n : ℕ) (f : ℕ → β) :
-  (range n).prod f = univ.prod (λ (k : fin n), f k) :=
-begin
-  symmetry,
-  refine prod_bij (λ k hk, k) _ _ _ _,
-  { rintro ⟨k, hk⟩ _, simp * },
-  { rintro ⟨k, hk⟩ _, simp * },
-  { intros, rwa fin.eq_iff_veq },
-  { intros k hk, rw mem_range at hk,
-    exact ⟨⟨k, hk⟩, mem_univ _, rfl⟩ }
-end
-
 section equiv
 
 open list equiv equiv.perm

src/data/fintype/card.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+-/
+
+import data.fintype
+import algebra.big_operators
+
+/-!
+Results about "big operations" over a `fintype`, and consequent
+results about cardinalities of certain types.
+
+## Implementation note
+This content had previously been in `data.fintype`, but was moved here to avoid
+requiring `algebra.big_operators` (and hence many other imports) as a
+dependency of `fintype`.
+-/
+
+universes u v
+
+variables {α : Type*} {β : Type*} {γ : Type*}
+
+namespace fintype
+
+lemma card_eq_sum_ones {α} [fintype α] : fintype.card α = (finset.univ : finset α).sum (λ _, 1) :=
+finset.card_eq_sum_ones _
+
+end fintype
+
+open finset
+
+theorem fin.prod_univ_succ [comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
+  univ.prod f = f 0 * univ.prod (λ i:fin n, f i.succ) :=
+begin
+  rw [fin.univ_succ, prod_insert, prod_image],
+  { intros x _ y _ hxy, exact fin.succ.inj hxy },
+  { simpa using fin.succ_ne_zero }
+end
+
+@[simp, to_additive] theorem fin.prod_univ_zero [comm_monoid β] (f : fin 0 → β) : univ.prod f = 1 := rfl
+
+theorem fin.sum_univ_succ [add_comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
+  univ.sum f = f 0 + univ.sum (λ i:fin n, f i.succ) :=
+by apply @fin.prod_univ_succ (multiplicative β)
+
+attribute [to_additive] fin.prod_univ_succ
+
+theorem fin.prod_univ_cast_succ [comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
+  univ.prod f = univ.prod (λ i:fin n, f i.cast_succ) * f (fin.last n) :=
+begin
+  rw [fin.univ_cast_succ, prod_insert, prod_image, mul_comm],
+  { intros x _ y _ hxy, exact fin.cast_succ_inj.mp hxy },
+  { simpa using fin.cast_succ_ne_last }
+end
+
+theorem fin.sum_univ_cast_succ [add_comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
+  univ.sum f = univ.sum (λ i:fin n, f i.cast_succ) + f (fin.last n) :=
+by apply @fin.prod_univ_cast_succ (multiplicative β)
+attribute [to_additive] fin.prod_univ_cast_succ
+
+@[simp] theorem fintype.card_sigma {α : Type*} (β : α → Type*)
+  [fintype α] [∀ a, fintype (β a)] :
+  fintype.card (sigma β) = univ.sum (λ a, fintype.card (β a)) :=
+card_sigma _ _
+
+-- FIXME ouch, this should be in the main file.
+@[simp] theorem fintype.card_sum (α β : Type*) [fintype α] [fintype β] :
+  fintype.card (α ⊕ β) = fintype.card α + fintype.card β :=
+by rw [sum.fintype, fintype.of_equiv_card]; simp
+
+@[simp] lemma fintype.card_pi {β : α → Type*} [fintype α] [decidable_eq α]
+  [f : Π a, fintype (β a)] : fintype.card (Π a, β a) = univ.prod (λ a, fintype.card (β a)) :=
+by letI f' : fintype (Πa∈univ, β a) :=
+  ⟨(univ.pi $ λa, univ), assume f, finset.mem_pi.2 $ assume a ha, mem_univ _⟩;
+exact calc fintype.card (Π a, β a) = fintype.card (Π a ∈ univ, β a) : fintype.card_congr
+  ⟨λ f a ha, f a, λ f a, f a (mem_univ a), λ _, rfl, λ _, rfl⟩
+... = univ.prod (λ a, fintype.card (β a)) : finset.card_pi _ _
+
+-- FIXME ouch, this should be in the main file.
+@[simp] lemma fintype.card_fun [fintype α] [decidable_eq α] [fintype β] :
+  fintype.card (α → β) = fintype.card β ^ fintype.card α :=
+by rw [fintype.card_pi, finset.prod_const, nat.pow_eq_pow]; refl
+
+@[simp] lemma card_vector [fintype α] (n : ℕ) :
+  fintype.card (vector α n) = fintype.card α ^ n :=
+by rw fintype.of_equiv_card; simp
+
+
+@[simp, to_additive]
+lemma finset.prod_attach_univ [fintype α] [comm_monoid β] (f : {a : α // a ∈ @univ α _} → β) :
+  univ.attach.prod (λ x, f x) = univ.prod (λ x, f ⟨x, (mem_univ _)⟩) :=
+prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp) (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩)
+
+@[to_additive]
+lemma finset.range_prod_eq_univ_prod [comm_monoid β] (n : ℕ) (f : ℕ → β) :
+  (range n).prod f = univ.prod (λ (k : fin n), f k) :=
+begin
+  symmetry,
+  refine prod_bij (λ k hk, k) _ _ _ _,
+  { rintro ⟨k, hk⟩ _, simp * },
+  { rintro ⟨k, hk⟩ _, simp * },
+  { intros, rwa fin.eq_iff_veq },
+  { intros k hk, rw mem_range at hk,
+    exact ⟨⟨k, hk⟩, mem_univ _, rfl⟩ }
+end

src/data/set/finite.lean

@@ -7,6 +7,7 @@ Finite sets.
 -/
 import logic.function
 import data.nat.basic data.fintype data.set.lattice data.set.function
+import algebra.big_operators
 
 open set lattice function
 

src/group_theory/perm/sign.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import data.fintype
+import algebra.big_operators
 
 universes u v
 open equiv function fintype finset

src/group_theory/sylow.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes
 -/
 import group_theory.group_action group_theory.quotient_group
 import group_theory.order_of_element data.zmod.basic
+import data.fintype.card
 
 open equiv fintype finset mul_action function
 open equiv.perm is_subgroup list quotient_group

src/linear_algebra/basis.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
 -/
 
 import linear_algebra.basic linear_algebra.finsupp order.zorn
+import data.fintype.card
 
 /-!
 

src/linear_algebra/determinant.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau, Chris Hughes, Tim Baanen
 -/
 import data.matrix.basic
 import data.matrix.pequiv
+import data.fintype.card
 import group_theory.perm.sign
 
 universes u v
@@ -84,7 +85,7 @@ calc det (M ⬝ N) = univ.sum (λ σ : perm n, (univ.pi (λ a, univ)).sum
   finset.sum_comm
 ... = ((@univ (n → n) _).filter bijective).sum (λ p : n → n, univ.sum
     (λ σ : perm n, ε σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
-  eq.symm $ sum_subset (filter_subset _) 
+  eq.symm $ sum_subset (filter_subset _)
     (λ f _ hbij, det_mul_aux $ by simpa using hbij)
 ... = (@univ (perm n) _).sum (λ τ, univ.sum
     (λ σ : perm n, ε σ * univ.prod (λ i, M (σ i) (τ i) * N (τ i) i))) :

src/number_theory/bernoulli.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin
 
 import data.rat
 import data.fintype
+import data.fintype.card
 
 /-!
 # Bernoulli numbers