From 62dd6a3df62c641149c81a913ea4ab05aaab2d5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 30 Apr 2024 05:21:39 +0000 Subject: [PATCH] feat: More big operator lemmas (#10551) From LeanAPAP --- Mathlib/Algebra/BigOperators/Basic.lean | 85 +++++++++++++++++++++++- Mathlib/Algebra/BigOperators/Ring.lean | 28 +++++++- Mathlib/Algebra/Module/BigOperators.lean | 17 ++++- Mathlib/Data/Finset/Basic.lean | 2 +- Mathlib/Data/Finset/Union.lean | 22 +++--- Mathlib/Data/Fintype/BigOperators.lean | 66 +++++++++++++----- Mathlib/Data/Fintype/Pi.lean | 33 ++++++++- Mathlib/GroupTheory/PGroup.lean | 2 +- 8 files changed, 223 insertions(+), 32 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index 15ea60d67ee31f..61336b054127c3 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -667,6 +667,19 @@ lemma prod_of_injOn (e : ι → κ) (he : Set.InjOn e s) (hest : Set.MapsTo e s variable [DecidableEq κ] +@[to_additive] +lemma prod_fiberwise_eq_prod_filter (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → α) : + ∏ j in t, ∏ i in s.filter fun i ↦ g i = j, f i = ∏ i in s.filter fun i ↦ g i ∈ t, f i := by + rw [← prod_disjiUnion, disjiUnion_filter_eq] + +@[to_additive] +lemma prod_fiberwise_eq_prod_filter' (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → α) : + ∏ j in t, ∏ _i in s.filter fun i ↦ g i = j, f j = ∏ i in s.filter fun i ↦ g i ∈ t, f (g i) := by + calc + _ = ∏ j in t, ∏ i in s.filter fun i ↦ g i = j, f (g i) := + prod_congr rfl fun j _ ↦ prod_congr rfl fun i hi ↦ by rw [(mem_filter.1 hi).2] + _ = _ := prod_fiberwise_eq_prod_filter _ _ _ _ + @[to_additive] lemma prod_fiberwise_of_maps_to {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → α) : ∏ j in t, ∏ i in s.filter fun i ↦ g i = j, f i = ∏ i in s, f i := by @@ -1945,6 +1958,23 @@ theorem prod_dvd_prod_of_subset {ι M : Type*} [CommMonoid M] (s t : Finset ι) end CommMonoid +section CancelCommMonoid +variable [DecidableEq ι] [CancelCommMonoid α] {s t : Finset ι} {f : ι → α} + +@[to_additive] +lemma prod_sdiff_eq_prod_sdiff_iff : + ∏ i in s \ t, f i = ∏ i in t \ s, f i ↔ ∏ i in s, f i = ∏ i in t, f i := + eq_comm.trans $ eq_iff_eq_of_mul_eq_mul $ by + rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left, + sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm] + +@[to_additive] +lemma prod_sdiff_ne_prod_sdiff_iff : + ∏ i in s \ t, f i ≠ ∏ i in t \ s, f i ↔ ∏ i in s, f i ≠ ∏ i in t, f i := + prod_sdiff_eq_prod_sdiff_iff.not + +end CancelCommMonoid + theorem card_eq_sum_ones (s : Finset α) : s.card = ∑ x in s, 1 := by rw [sum_const, smul_eq_mul, mul_one] #align finset.card_eq_sum_ones Finset.card_eq_sum_ones @@ -1955,6 +1985,10 @@ theorem sum_const_nat {m : ℕ} {f : α → ℕ} (h₁ : ∀ x ∈ s, f x = m) : apply sum_congr rfl h₁ #align finset.sum_const_nat Finset.sum_const_nat +lemma sum_card_fiberwise_eq_card_filter {κ : Type*} [DecidableEq κ] (s : Finset ι) (t : Finset κ) + (g : ι → κ) : ∑ j in t, (s.filter fun i ↦ g i = j).card = (s.filter fun i ↦ g i ∈ t).card := by + simpa only [card_eq_sum_ones] using sum_fiberwise_eq_sum_filter _ _ _ _ + lemma card_filter (p) [DecidablePred p] (s : Finset α) : (filter p s).card = ∑ a in s, ite (p a) 1 0 := by rw [sum_ite, sum_const_zero, add_zero, sum_const, smul_eq_mul, mul_one] @@ -2156,10 +2190,13 @@ theorem prod_int_mod (s : Finset α) (n : ℤ) (f : α → ℤ) : end Finset namespace Fintype -variable {ι κ α : Type*} [Fintype ι] [Fintype κ] [CommMonoid α] +variable {ι κ α : Type*} [Fintype ι] [Fintype κ] open Finset +section CommMonoid +variable [CommMonoid α] + /-- `Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.Bijective`. See `Function.Bijective.prod_comp` for a version without `h`. -/ @@ -2256,6 +2293,52 @@ theorem prod_subtype_mul_prod_subtype {α β : Type*} [Fintype α] [CommMonoid #align fintype.prod_subtype_mul_prod_subtype Fintype.prod_subtype_mul_prod_subtype #align fintype.sum_subtype_add_sum_subtype Fintype.sum_subtype_add_sum_subtype +@[to_additive] lemma prod_subset {s : Finset ι} {f : ι → α} (h : ∀ i, f i ≠ 1 → i ∈ s) : + ∏ i in s, f i = ∏ i, f i := + Finset.prod_subset s.subset_univ $ by simpa [not_imp_comm (a := _ ∈ s)] + +@[to_additive] +lemma prod_ite_eq_ite_exists (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) + (a : α) : ∏ i, ite (p i) a 1 = ite (∃ i, p i) a 1 := by + simp [prod_ite_one univ p (by simpa using h)] + +variable [DecidableEq ι] + +/-- See also `Finset.prod_dite_eq`. -/ +@[to_additive "See also `Finset.sum_dite_eq`."] lemma prod_dite_eq (i : ι) (f : ∀ j, i = j → α) : + ∏ j, (if h : i = j then f j h else 1) = f i rfl := by + rw [Finset.prod_dite_eq, if_pos (mem_univ _)] + +/-- See also `Finset.prod_dite_eq'`. -/ +@[to_additive "See also `Finset.sum_dite_eq'`."] lemma prod_dite_eq' (i : ι) (f : ∀ j, j = i → α) : + ∏ j, (if h : j = i then f j h else 1) = f i rfl := by + rw [Finset.prod_dite_eq', if_pos (mem_univ _)] + +/-- See also `Finset.prod_ite_eq`. -/ +@[to_additive "See also `Finset.sum_ite_eq`."] +lemma prod_ite_eq (i : ι) (f : ι → α) : ∏ j, (if i = j then f j else 1) = f i := by + rw [Finset.prod_ite_eq, if_pos (mem_univ _)] + +/-- See also `Finset.prod_ite_eq'`. -/ +@[to_additive "See also `Finset.sum_ite_eq'`."] +lemma prod_ite_eq' (i : ι) (f : ι → α) : ∏ j, (if j = i then f j else 1) = f i := by + rw [Finset.prod_ite_eq', if_pos (mem_univ _)] + +/-- See also `Finset.prod_pi_mulSingle`. -/ +@[to_additive "See also `Finset.sum_pi_single`."] +lemma prod_pi_mulSingle {α : ι → Type*} [∀ i, CommMonoid (α i)] (i : ι) (f : ∀ i, α i) : + ∏ j, Pi.mulSingle j (f j) i = f i := prod_dite_eq _ _ + +/-- See also `Finset.prod_pi_mulSingle'`. -/ +@[to_additive "See also `Finset.sum_pi_single'`."] +lemma prod_pi_mulSingle' (i : ι) (a : α) : ∏ j, Pi.mulSingle i a j = a := prod_dite_eq' _ _ + +end CommMonoid + +variable [CommMonoidWithZero α] {p : ι → Prop} [DecidablePred p] + +lemma prod_boole : ∏ i, ite (p i) (1 : α) 0 = ite (∀ i, p i) 1 0 := by simp [Finset.prod_boole] + end Fintype namespace Finset diff --git a/Mathlib/Algebra/BigOperators/Ring.lean b/Mathlib/Algebra/BigOperators/Ring.lean index 25e509f2bdcc95..cb8c3ad8d10d0a 100644 --- a/Mathlib/Algebra/BigOperators/Ring.lean +++ b/Mathlib/Algebra/BigOperators/Ring.lean @@ -170,11 +170,11 @@ lemma prod_univ_sum [Fintype ι] (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → lemma sum_prod_piFinset {κ : Type*} [Fintype ι] (s : Finset κ) (g : ι → κ → α) : ∑ f in piFinset fun _ : ι ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j in s, g i j := by - classical rw [← prod_univ_sum] + rw [← prod_univ_sum] lemma sum_pow' (s : Finset ι) (f : ι → α) (n : ℕ) : (∑ a in s, f a) ^ n = ∑ p in piFinset fun _i : Fin n ↦ s, ∏ i, f (p i) := by - classical convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp + convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp /-- The product of `f a + g a` over all of `s` is the sum over the powerset of `s` of the product of `f` over a subset `t` times the product of `g` over the complement of `t` -/ @@ -297,7 +297,31 @@ lemma sum_div (s : Finset ι) (f : ι → α) (a : α) : end DivisionSemiring end Finset +open Finset + +namespace Fintype +variable {ι κ α : Type*} [DecidableEq ι] [Fintype ι] [Fintype κ] [CommSemiring α] + +lemma sum_pow (f : ι → α) (n : ℕ) : (∑ a, f a) ^ n = ∑ p : Fin n → ι, ∏ i, f (p i) := by + simp [sum_pow'] + +lemma sum_mul_sum (f : ι → α) (g : κ → α) : (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j := + Finset.sum_mul_sum _ _ _ _ + +lemma prod_add (f g : ι → α) : ∏ a, (f a + g a) = ∑ t, (∏ a in t, f a) * ∏ a in tᶜ, g a := by + simpa [compl_eq_univ_sdiff] using Finset.prod_add f g univ + +end Fintype + namespace Nat +variable {ι : Type*} {s : Finset ι} {f : ι → ℕ} {n : ℕ} + +protected lemma sum_div (hf : ∀ i ∈ s, n ∣ f i) : (∑ i in s, f i) / n = ∑ i in s, f i / n := by + obtain rfl | hn := n.eq_zero_or_pos + · simp + rw [Nat.div_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul] + refine' sum_congr rfl fun s hs ↦ _ + rw [Nat.div_mul_cancel (hf _ hs)] @[simp, norm_cast] lemma cast_list_sum [AddMonoidWithOne β] (s : List ℕ) : (↑s.sum : β) = (s.map (↑)).sum := diff --git a/Mathlib/Algebra/Module/BigOperators.lean b/Mathlib/Algebra/Module/BigOperators.lean index 9336ac2f708061..977c708bca13f4 100644 --- a/Mathlib/Algebra/Module/BigOperators.lean +++ b/Mathlib/Algebra/Module/BigOperators.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes, Yury Kudryashov, Yaël Dillies -/ import Mathlib.Algebra.Module.Defs +import Mathlib.Data.Fintype.BigOperators import Mathlib.GroupTheory.GroupAction.BigOperators #align_import algebra.module.big_operators from "leanprover-community/mathlib"@"509de852e1de55e1efa8eacfa11df0823f26f226" @@ -14,7 +15,7 @@ import Mathlib.GroupTheory.GroupAction.BigOperators open BigOperators -variable {α β R M ι : Type*} +variable {ι κ α β R M : Type*} section AddCommMonoid @@ -51,3 +52,17 @@ end AddCommMonoid theorem Finset.cast_card [CommSemiring R] (s : Finset α) : (s.card : R) = ∑ a in s, 1 := by rw [Finset.sum_const, Nat.smul_one_eq_coe] #align finset.cast_card Finset.cast_card + +open Finset + +namespace Fintype +variable [DecidableEq ι] [Fintype ι] [AddCommMonoid α] + +lemma sum_piFinset_apply (f : κ → α) (s : Finset κ) (i : ι) : + ∑ g in piFinset fun _ : ι ↦ s, f (g i) = s.card ^ (card ι - 1) • ∑ b in s, f b := by + classical + rw [Finset.sum_comp] + simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum, + sum_ite_mem, inter_self] + +end Fintype diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean index b9c09175770acf..d6f3f575dcdd67 100644 --- a/Mathlib/Data/Finset/Basic.lean +++ b/Mathlib/Data/Finset/Basic.lean @@ -2631,7 +2631,7 @@ theorem filter_False {h} (s : Finset α) : @filter _ (fun _ => False) h s = ∅ variable {p q} -theorem filter_eq_self : s.filter p = s ↔ ∀ x ∈ s, p x := by simp [Finset.ext_iff] +@[simp] lemma filter_eq_self : s.filter p = s ↔ ∀ x ∈ s, p x := by simp [Finset.ext_iff] #align finset.filter_eq_self Finset.filter_eq_self theorem filter_eq_empty_iff : s.filter p = ∅ ↔ ∀ ⦃x⦄, x ∈ s → ¬p x := by simp [Finset.ext_iff] diff --git a/Mathlib/Data/Finset/Union.lean b/Mathlib/Data/Finset/Union.lean index 1bc57a67df11d9..2b57154d48d63c 100644 --- a/Mathlib/Data/Finset/Union.lean +++ b/Mathlib/Data/Finset/Union.lean @@ -88,14 +88,20 @@ lemma disjiUnion_disjiUnion (s : Finset α) (f : α → Finset β) (g : β → F eq_of_veq <| Multiset.bind_assoc.trans (Multiset.attach_bind_coe _ _).symm #align finset.disj_Union_disj_Union Finset.disjiUnion_disjiUnion -lemma disjiUnion_filter_eq_of_maps_to [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} - (h : ∀ x ∈ s, f x ∈ t) : - t.disjiUnion (fun a ↦ s.filter (fun c ↦ f c = a)) - (fun x' hx y' hy hne ↦ by - simp_rw [disjoint_left, mem_filter] - rintro i ⟨_, rfl⟩ ⟨_, rfl⟩ - exact hne rfl) = s := - ext fun b ↦ by simpa using h b +variable [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} + +private lemma pairwiseDisjoint_fibers : Set.PairwiseDisjoint ↑t fun a ↦ s.filter (f · = a) := + fun x' hx y' hy hne ↦ by + simp_rw [disjoint_left, mem_filter]; rintro i ⟨_, rfl⟩ ⟨_, rfl⟩; exact hne rfl + +-- `simpNF` claims that the statement can't simplify itself, but it can (as of 2024-02-14) +@[simp, nolint simpNF] lemma disjiUnion_filter_eq (s : Finset α) (t : Finset β) (f : α → β) : + t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = + s.filter fun c ↦ f c ∈ t := + ext fun b => by simpa using and_comm + +lemma disjiUnion_filter_eq_of_maps_to (h : ∀ x ∈ s, f x ∈ t) : + t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = s := by simpa #align finset.disj_Union_filter_eq_of_maps_to Finset.disjiUnion_filter_eq_of_maps_to end DisjiUnion diff --git a/Mathlib/Data/Fintype/BigOperators.lean b/Mathlib/Data/Fintype/BigOperators.lean index 10bb80f39daae3..3254aaf8e0e309 100644 --- a/Mathlib/Data/Fintype/BigOperators.lean +++ b/Mathlib/Data/Fintype/BigOperators.lean @@ -118,29 +118,63 @@ end open Finset -@[simp] -nonrec theorem Fintype.card_sigma {α : Type*} (β : α → Type*) [Fintype α] [∀ a, Fintype (β a)] : - Fintype.card (Sigma β) = ∑ a, Fintype.card (β a) := - card_sigma _ _ -#align fintype.card_sigma Fintype.card_sigma +section Pi +variable {ι κ : Type*} {α : ι → Type*} [DecidableEq ι] [DecidableEq κ] [Fintype ι] + [∀ i, DecidableEq (α i)] -@[simp] -theorem Finset.card_pi [DecidableEq α] {δ : α → Type*} (s : Finset α) (t : ∀ a, Finset (δ a)) : - (s.pi t).card = ∏ a in s, card (t a) := - Multiset.card_pi _ _ +@[simp] lemma Finset.card_pi (s : Finset ι) (t : ∀ i, Finset (α i)) : + (s.pi t).card = ∏ i in s, card (t i) := Multiset.card_pi _ _ #align finset.card_pi Finset.card_pi -@[simp] -theorem Fintype.card_piFinset [DecidableEq α] [Fintype α] {δ : α → Type*} (t : ∀ a, Finset (δ a)) : - (Fintype.piFinset t).card = ∏ a, Finset.card (t a) := by simp [Fintype.piFinset, card_map] +namespace Fintype + +@[simp] lemma card_piFinset (s : ∀ i, Finset (α i)) : + (piFinset s).card = ∏ i, (s i).card := by simp [piFinset, card_map] #align fintype.card_pi_finset Fintype.card_piFinset -@[simp] -theorem Fintype.card_pi {β : α → Type*} [DecidableEq α] [Fintype α] [∀ a, Fintype (β a)] : - Fintype.card (∀ a, β a) = ∏ a, Fintype.card (β a) := - Fintype.card_piFinset _ +@[simp] lemma card_pi [DecidableEq ι] [∀ i, Fintype (α i)] : card (∀ i, α i) = ∏ i, card (α i) := + card_piFinset _ #align fintype.card_pi Fintype.card_pi +@[simp] nonrec lemma card_sigma [Fintype ι] [∀ i, Fintype (α i)] : + card (Sigma α) = ∑ i, card (α i) := card_sigma _ _ +#align fintype.card_sigma Fintype.card_sigma + +/-- The number of dependent maps `f : Π j, s j` for which the `i` component is `a` is the product +over all `j ≠ i` of `(s j).card`. + +Note that this is just a composition of easier lemmas, but there's some glue missing to make that +smooth enough not to need this lemma. -/ +lemma card_filter_piFinset_eq_of_mem (s : ∀ i, Finset (α i)) (i : ι) {a : α i} (ha : a ∈ s i) : + ((piFinset s).filter fun f ↦ f i = a).card = ∏ j in univ.erase i, (s j).card := by + calc + _ = ∏ j, (Function.update s i {a} j).card := by + rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset] + _ = ∏ j, Function.update (fun j ↦ (s j).card) i 1 j := + Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*] + _ = _ := by simp [prod_update_of_mem, erase_eq] + +lemma card_filter_piFinset_const_eq_of_mem (s : Finset κ) (i : ι) {x : κ} (hx : x ∈ s) : + ((piFinset fun _ ↦ s).filter fun f ↦ f i = x).card = s.card ^ (card ι - 1) := + (card_filter_piFinset_eq_of_mem _ _ hx).trans $ by + rw [prod_const s.card, card_erase_of_mem (mem_univ _), card_univ] + +lemma card_filter_piFinset_eq (s : ∀ i, Finset (α i)) (i : ι) (a : α i) : + ((piFinset s).filter fun f ↦ f i = a).card = + if a ∈ s i then ∏ b in univ.erase i, (s b).card else 0 := by + split_ifs with h + · rw [card_filter_piFinset_eq_of_mem _ _ h] + · rw [filter_piFinset_of_not_mem _ _ _ h, Finset.card_empty] + +lemma card_filter_piFinset_const (s : Finset κ) (i : ι) (j : κ) : + ((piFinset fun _ ↦ s).filter fun f ↦ f i = j).card = + if j ∈ s then s.card ^ (card ι - 1) else 0 := + (card_filter_piFinset_eq _ _ _).trans $ by + rw [prod_const s.card, card_erase_of_mem (mem_univ _), card_univ] + +end Fintype +end Pi + -- FIXME ouch, this should be in the main file. @[simp] theorem Fintype.card_fun [DecidableEq α] [Fintype α] [Fintype β] : diff --git a/Mathlib/Data/Fintype/Pi.lean b/Mathlib/Data/Fintype/Pi.lean index 32bcb195258d28..acb5e00bf4c57a 100644 --- a/Mathlib/Data/Fintype/Pi.lean +++ b/Mathlib/Data/Fintype/Pi.lean @@ -97,10 +97,39 @@ lemma eval_image_piFinset (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a choose f hf using ht exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩ -lemma filter_piFinset_of_not_mem [∀ a, DecidableEq (δ a)] (t : ∀ a, Finset (δ a)) (a : α) - (x : δ a) (hx : x ∉ t a) : (piFinset t).filter (· a = x) = ∅ := by +lemma eval_image_piFinset_const {β} [DecidableEq β] (t : Finset β) (a : α) : + ((piFinset fun _i : α ↦ t).image fun f ↦ f a) = t := by + obtain rfl | ht := t.eq_empty_or_nonempty + · haveI : Nonempty α := ⟨a⟩ + simp + · exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht + +variable [∀ a, DecidableEq (δ a)] + +lemma filter_piFinset_of_not_mem (t : ∀ a, Finset (δ a)) (a : α) (x : δ a) (hx : x ∉ t a) : + (piFinset t).filter (· a = x) = ∅ := by simp only [filter_eq_empty_iff, mem_piFinset]; rintro f hf rfl; exact hx (hf _) +-- TODO: This proof looks like a good example of something that `aesop` can't do but should +lemma piFinset_update_eq_filter_piFinset_mem (s : ∀ i, Finset (δ i)) (i : α) {t : Finset (δ i)} + (hts : t ⊆ s i) : piFinset (Function.update s i t) = (piFinset s).filter (fun f ↦ f i ∈ t) := by + ext f + simp only [mem_piFinset, mem_filter] + refine ⟨fun h ↦ ?_, fun h j ↦ ?_⟩ + · have := by simpa using h i + refine ⟨fun j ↦ ?_, this⟩ + obtain rfl | hji := eq_or_ne j i + · exact hts this + · simpa [hji] using h j + · obtain rfl | hji := eq_or_ne j i + · simpa using h.2 + · simpa [hji] using h.1 j + +lemma piFinset_update_singleton_eq_filter_piFinset_eq (s : ∀ i, Finset (δ i)) (i : α) {a : δ i} + (ha : a ∈ s i) : + piFinset (Function.update s i {a}) = (piFinset s).filter (fun f ↦ f i = a) := by + simp [piFinset_update_eq_filter_piFinset_mem, ha] + end Fintype /-! ### pi -/ diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean index 72ac5ceb9c7fe5..0ed2e000733cbd 100644 --- a/Mathlib/GroupTheory/PGroup.lean +++ b/Mathlib/GroupTheory/PGroup.lean @@ -187,7 +187,7 @@ theorem card_modEq_card_fixedPoints [Fintype (fixedPoints G α)] : calc card α = card (Σy : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) := card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm - _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma _ + _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_ _ = _ := by simp; rfl rw [← ZMod.eq_iff_modEq_nat p, Nat.cast_sum, Nat.cast_sum]