From 31263840fccb6bc5ea3d3d49676a1d16d596cfc0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 14 Oct 2022 23:58:26 +0000 Subject: [PATCH] refactor(data/finset/noncomm_prod): Use `set.pairwise` (#16859) Redefine the various `noncomm_prod`s using `set.pairwise`. This has the advantage of having a solid API around monotonicity in the set or in the relation and avoiding checking the trivial `i = j` case. --- src/algebra/group/commute.lean | 6 + src/analysis/normed_space/exponential.lean | 13 +- .../normed_space/matrix_exponential.lean | 4 +- src/data/finset/basic.lean | 3 + src/data/finset/noncomm_prod.lean | 232 +++++++----------- src/data/finset/pairwise.lean | 19 +- src/data/list/nodup.lean | 14 +- src/group_theory/noncomm_pi_coprod.lean | 5 +- src/group_theory/perm/cycle/basic.lean | 68 ++--- src/group_theory/perm/cycle/type.lean | 6 +- src/group_theory/perm/support.lean | 2 + src/group_theory/subgroup/basic.lean | 18 +- src/group_theory/submonoid/membership.lean | 7 +- 13 files changed, 160 insertions(+), 237 deletions(-) diff --git a/src/algebra/group/commute.lean b/src/algebra/group/commute.lean index 0a52ee04dedee..80133fc0323cf 100644 --- a/src/algebra/group/commute.lean +++ b/src/algebra/group/commute.lean @@ -54,6 +54,12 @@ protected lemma symm {a b : S} (h : commute a b) : commute b a := eq.symm h protected theorem symm_iff {a b : S} : commute a b ↔ commute b a := ⟨commute.symm, commute.symm⟩ +@[to_additive] instance : is_refl S commute := ⟨commute.refl⟩ + +-- This instance is useful for `finset.noncomm_prod` +@[to_additive] instance on_is_refl {f : G → S} : is_refl G (λ a b, commute (f a) (f b)) := +⟨λ _, commute.refl _⟩ + end has_mul section semigroup diff --git a/src/analysis/normed_space/exponential.lean b/src/analysis/normed_space/exponential.lean index 81581cc4ea78e..882cf9621fcde 100644 --- a/src/analysis/normed_space/exponential.lean +++ b/src/analysis/normed_space/exponential.lean @@ -452,18 +452,17 @@ end /-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually commute then `exp 𝕂 (∑ i, f i) = ∏ i, exp 𝕂 (f i)`. -/ lemma exp_sum_of_commute {ι} (s : finset ι) (f : ι → 𝔸) - (h : ∀ (i ∈ s) (j ∈ s), commute (f i) (f j)) : + (h : (s : set ι).pairwise $ λ i j, commute (f i) (f j)) : exp 𝕂 (∑ i in s, f i) = s.noncomm_prod (λ i, exp 𝕂 (f i)) - (λ i hi j hj, (h i hi j hj).exp 𝕂) := + (λ i hi j hj _, (h.of_refl hi hj).exp 𝕂) := begin classical, induction s using finset.induction_on with a s ha ih, { simp }, rw [finset.noncomm_prod_insert_of_not_mem _ _ _ _ ha, finset.sum_insert ha, - exp_add_of_commute, ih], - refine commute.sum_right _ _ _ _, - intros i hi, - exact h _ (finset.mem_insert_self _ _) _ (finset.mem_insert_of_mem hi), + exp_add_of_commute, ih (h.mono $ finset.subset_insert _ _)], + refine commute.sum_right _ _ _ (λ i hi, _), + exact h.of_refl (finset.mem_insert_self _ _) (finset.mem_insert_of_mem hi), end lemma exp_nsmul (n : ℕ) (x : 𝔸) : @@ -591,7 +590,7 @@ lemma exp_sum {ι} (s : finset ι) (f : ι → 𝔸) : exp 𝕂 (∑ i in s, f i) = ∏ i in s, exp 𝕂 (f i) := begin rw [exp_sum_of_commute, finset.noncomm_prod_eq_prod], - exact λ i hi j hj, commute.all _ _, + exact λ i hi j hj _, commute.all _ _, end end comm_algebra diff --git a/src/analysis/normed_space/matrix_exponential.lean b/src/analysis/normed_space/matrix_exponential.lean index 1a1aea1e5afa5..423ad6dfbd9ea 100644 --- a/src/analysis/normed_space/matrix_exponential.lean +++ b/src/analysis/normed_space/matrix_exponential.lean @@ -149,9 +149,9 @@ begin end lemma exp_sum_of_commute {ι} (s : finset ι) (f : ι → matrix m m 𝔸) - (h : ∀ (i ∈ s) (j ∈ s), commute (f i) (f j)) : + (h : (s : set ι).pairwise $ λ i j, commute (f i) (f j)) : exp 𝕂 (∑ i in s, f i) = s.noncomm_prod (λ i, exp 𝕂 (f i)) - (λ i hi j hj, (h i hi j hj).exp 𝕂) := + (λ i hi j hj _, (h.of_refl hi hj).exp 𝕂) := begin letI : semi_normed_ring (matrix m m 𝔸) := matrix.linfty_op_semi_normed_ring, letI : normed_ring (matrix m m 𝔸) := matrix.linfty_op_normed_ring, diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index 36c919d376986..7aefff28180fa 100644 --- a/src/data/finset/basic.lean +++ b/src/data/finset/basic.lean @@ -2025,6 +2025,9 @@ def to_finset (l : list α) : finset α := multiset.to_finset l lemma to_finset_eq (n : nodup l) : @finset.mk α l n = l.to_finset := multiset.to_finset_eq n @[simp] lemma mem_to_finset : a ∈ l.to_finset ↔ a ∈ l := mem_dedup +@[simp, norm_cast] lemma coe_to_finset (l : list α) : (l.to_finset : set α) = {a | a ∈ l} := +set.ext $ λ _, list.mem_to_finset + @[simp] lemma to_finset_nil : to_finset (@nil α) = ∅ := rfl @[simp] lemma to_finset_cons : to_finset (a :: l) = insert a (to_finset l) := diff --git a/src/data/finset/noncomm_prod.lean b/src/data/finset/noncomm_prod.lean index 5cef6169bb93b..be920fd0a5a3d 100644 --- a/src/data/finset/noncomm_prod.lean +++ b/src/data/finset/noncomm_prod.lean @@ -27,18 +27,21 @@ the two must be equal. -/ -variables {α β γ : Type*} (f : α → β → β) (op : α → α → α) +variables {F ι α β γ : Type*} (f : α → β → β) (op : α → α → α) namespace multiset /-- Fold of a `s : multiset α` with `f : α → β → β`, given a proof that `left_commutative f` on all elements `x ∈ s`. -/ -def noncomm_foldr (s : multiset α) (comm : ∀ (x ∈ s) (y ∈ s) b, f x (f y b) = f y (f x b)) (b : β) : +def noncomm_foldr (s : multiset α) + (comm : {x | x ∈ s}.pairwise $ λ x y, ∀ b, f x (f y b) = f y (f x b)) (b : β) : β := -s.attach.foldr (f ∘ subtype.val) (λ ⟨x, hx⟩ ⟨y, hy⟩, comm x hx y hy) b +s.attach.foldr (f ∘ subtype.val) (λ ⟨x, hx⟩ ⟨y, hy⟩, begin + haveI : is_refl α (λ x y, ∀ b, f x (f y b) = f y (f x b)) := ⟨λ x b, rfl⟩, + exact comm.of_refl hx hy, + end) b -@[simp] lemma noncomm_foldr_coe (l : list α) - (comm : ∀ (x ∈ (l : multiset α)) (y ∈ (l : multiset α)) b, f x (f y b) = f y (f x b)) (b : β) : +@[simp] lemma noncomm_foldr_coe (l : list α) (comm) (b : β) : noncomm_foldr f (l : multiset α) comm b = l.foldr f b := begin simp only [noncomm_foldr, coe_foldr, coe_attach, list.attach], @@ -46,14 +49,9 @@ begin simp [list.map_pmap, list.pmap_eq_map] end -@[simp] lemma noncomm_foldr_empty - (h : ∀ (x ∈ (0 : multiset α)) (y ∈ (0 : multiset α)) b, f x (f y b) = f y (f x b)) (b : β) : - noncomm_foldr f (0 : multiset α) h b = b := rfl +@[simp] lemma noncomm_foldr_empty (h) (b : β) : noncomm_foldr f (0 : multiset α) h b = b := rfl -lemma noncomm_foldr_cons (s : multiset α) (a : α) - (h : ∀ (x ∈ (a ::ₘ s)) (y ∈ (a ::ₘ s)) b, f x (f y b) = f y (f x b)) - (h' : ∀ (x ∈ s) (y ∈ s) b, f x (f y b) = f y (f x b)) - (b : β) : +lemma noncomm_foldr_cons (s : multiset α) (a : α) (h h') (b : β) : noncomm_foldr f (a ::ₘ s) h b = f a (noncomm_foldr f s h' b) := begin induction s using quotient.induction_on, @@ -61,7 +59,7 @@ begin end lemma noncomm_foldr_eq_foldr (s : multiset α) (h : left_commutative f) (b : β) : - noncomm_foldr f s (λ x _ y _, h x y) b = foldr f h b s := + noncomm_foldr f s (λ x _ y _ _, h x y) b = foldr f h b s := begin induction s using quotient.induction_on, simp @@ -72,34 +70,24 @@ include assoc /-- Fold of a `s : multiset α` with an associative `op : α → α → α`, given a proofs that `op` is commutative on all elements `x ∈ s`. -/ -def noncomm_fold (s : multiset α) - (comm : ∀ (x ∈ s) (y ∈ s), op x y = op y x) - (a : α) : α := -noncomm_foldr op s (λ x hx y hy b, by rw [←assoc.assoc, comm _ hx _ hy, assoc.assoc]) a - -@[simp] lemma noncomm_fold_coe (l : list α) - (comm : ∀ (x ∈ (l : multiset α)) (y ∈ (l : multiset α)), op x y = op y x) - (a : α) : +def noncomm_fold (s : multiset α) (comm : {x | x ∈ s}.pairwise $ λ x y, op x y = op y x) : α → α := +noncomm_foldr op s (λ x hx y hy h b, by rw [←assoc.assoc, comm hx hy h, assoc.assoc]) + +@[simp] lemma noncomm_fold_coe (l : list α) (comm) (a : α) : noncomm_fold op (l : multiset α) comm a = l.foldr op a := by simp [noncomm_fold] -@[simp] lemma noncomm_fold_empty - (h : ∀ (x ∈ (0 : multiset α)) (y ∈ (0 : multiset α)), op x y = op y x) (a : α) : - noncomm_fold op (0 : multiset α) h a = a := rfl +@[simp] lemma noncomm_fold_empty (h) (a : α) : noncomm_fold op (0 : multiset α) h a = a := rfl -lemma noncomm_fold_cons (s : multiset α) (a : α) - (h : ∀ (x ∈ a ::ₘ s) (y ∈ a ::ₘ s), op x y = op y x) - (h' : ∀ (x ∈ s) (y ∈ s), op x y = op y x) - (x : α) : +lemma noncomm_fold_cons (s : multiset α) (a : α) (h h') (x : α) : noncomm_fold op (a ::ₘ s) h x = op a (noncomm_fold op s h' x) := begin induction s using quotient.induction_on, simp end -lemma noncomm_fold_eq_fold (s : multiset α) [is_commutative α op] - (a : α) : - noncomm_fold op s (λ x _ y _, is_commutative.comm x y) a = fold op a s := +lemma noncomm_fold_eq_fold (s : multiset α) [is_commutative α op] (a : α) : + noncomm_fold op s (λ x _ y _ _, is_commutative.comm x y) a = fold op a s := begin induction s using quotient.induction_on, simp @@ -112,11 +100,10 @@ variables [monoid α] [monoid β] on all elements `x ∈ s`. -/ @[to_additive "Sum of a `s : multiset α` with `[add_monoid α]`, given a proof that `+` commutes on all elements `x ∈ s`." ] -def noncomm_prod (s : multiset α) (comm : ∀ (x ∈ s) (y ∈ s), commute x y) : α := +def noncomm_prod (s : multiset α) (comm : {x | x ∈ s}.pairwise commute) : α := s.noncomm_fold (*) comm 1 -@[simp, to_additive] lemma noncomm_prod_coe (l : list α) - (comm : ∀ (x ∈ (l : multiset α)) (y ∈ (l : multiset α)), commute x y) : +@[simp, to_additive] lemma noncomm_prod_coe (l : list α) (comm) : noncomm_prod (l : multiset α) comm = l.prod := begin rw [noncomm_prod], @@ -125,26 +112,17 @@ begin { simp }, { rw [list.prod_cons, list.foldr, hl], intros x hx y hy, - exact comm x (list.mem_cons_of_mem _ hx) y (list.mem_cons_of_mem _ hy) } + exact comm (list.mem_cons_of_mem _ hx) (list.mem_cons_of_mem _ hy) } end -@[simp, to_additive] lemma noncomm_prod_empty - (h : ∀ (x ∈ (0 : multiset α)) (y ∈ (0 : multiset α)), commute x y) : - noncomm_prod (0 : multiset α) h = 1 := rfl +@[simp, to_additive] lemma noncomm_prod_empty (h) : noncomm_prod (0 : multiset α) h = 1 := rfl -@[simp, to_additive] lemma noncomm_prod_cons (s : multiset α) (a : α) - (comm : ∀ (x ∈ a ::ₘ s) (y ∈ a ::ₘ s), commute x y) : - noncomm_prod (a ::ₘ s) comm = a * noncomm_prod s - (λ x hx y hy, comm _ (mem_cons_of_mem hx) _ (mem_cons_of_mem hy)) := -begin - induction s using quotient.induction_on, - simp -end +@[simp, to_additive] lemma noncomm_prod_cons (s : multiset α) (a : α) (comm) : + noncomm_prod (a ::ₘ s) comm = a * noncomm_prod s (comm.mono $ λ _, mem_cons_of_mem) := +by { induction s using quotient.induction_on, simp } -@[to_additive] lemma noncomm_prod_cons' (s : multiset α) (a : α) - (comm : ∀ (x ∈ a ::ₘ s) (y ∈ a ::ₘ s), commute x y) : - noncomm_prod (a ::ₘ s) comm = noncomm_prod s - (λ x hx y hy, comm _ (mem_cons_of_mem hx) _ (mem_cons_of_mem hy)) * a := +@[to_additive] lemma noncomm_prod_cons' (s : multiset α) (a : α) (comm) : + noncomm_prod (a ::ₘ s) comm = noncomm_prod s (comm.mono $ λ _, mem_cons_of_mem) * a := begin induction s using quotient.induction_on with s, simp only [quot_mk_to_coe, cons_coe, noncomm_prod_coe, list.prod_cons], @@ -152,7 +130,7 @@ begin { simp }, { rw [list.prod_cons, mul_assoc, ←IH, ←mul_assoc, ←mul_assoc], { congr' 1, - apply comm; + apply comm.of_refl; simp }, { intros x hx y hy, simp only [quot_mk_to_coe, list.mem_cons_iff, mem_coe, cons_coe] at hx hy, @@ -164,28 +142,26 @@ begin end @[protected, to_additive] -lemma nocomm_prod_map_aux (s : multiset α) - (comm : ∀ (x ∈ s) (y ∈ s), commute x y) - {F : Type*} [monoid_hom_class F α β] (f : F) : - ∀ (x ∈ s.map f) (y ∈ s.map f), commute x y := +lemma noncomm_prod_map_aux [monoid_hom_class F α β] (s : multiset α) + (comm : {x | x ∈ s}.pairwise commute) (f : F) : + {x | x ∈ s.map f}.pairwise commute := begin simp only [multiset.mem_map], - rintros _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩, - exact (comm _ hx _ hy).map f, + rintros _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ _, + exact (comm.of_refl hx hy).map f, end @[to_additive] -lemma noncomm_prod_map (s : multiset α) (comm : ∀ (x ∈ s) (y ∈ s), commute x y) - {F : Type*} [monoid_hom_class F α β] (f : F) : - f (s.noncomm_prod comm) = (s.map f).noncomm_prod (nocomm_prod_map_aux s comm f) := +lemma noncomm_prod_map [monoid_hom_class F α β] (s : multiset α) (comm) (f : F) : + f (s.noncomm_prod comm) = (s.map f).noncomm_prod (noncomm_prod_map_aux s comm f) := begin induction s using quotient.induction_on, simpa using map_list_prod f _, end @[to_additive noncomm_sum_eq_card_nsmul] -lemma noncomm_prod_eq_pow_card (s : multiset α) (comm : ∀ (x ∈ s) (y ∈ s), commute x y) - (m : α) (h : ∀ (x ∈ s), x = m) : s.noncomm_prod comm = m ^ s.card := +lemma noncomm_prod_eq_pow_card (s : multiset α) (comm) (m : α) (h : ∀ x ∈ s, x = m) : + s.noncomm_prod comm = m ^ s.card := begin induction s using quotient.induction_on, simp only [quot_mk_to_coe, noncomm_prod_coe, coe_card, mem_coe] at *, @@ -193,16 +169,15 @@ begin end @[to_additive] lemma noncomm_prod_eq_prod {α : Type*} [comm_monoid α] (s : multiset α) : - noncomm_prod s (λ _ _ _ _, commute.all _ _) = prod s := + noncomm_prod s (λ _ _ _ _ _, commute.all _ _) = prod s := begin induction s using quotient.induction_on, simp end @[to_additive noncomm_sum_add_commute] -lemma noncomm_prod_commute (s : multiset α) - (comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute x y) - (y : α) (h : ∀ (x : α), x ∈ s → commute y x) : commute y (s.noncomm_prod comm) := +lemma noncomm_prod_commute (s : multiset α) (comm) (y : α) (h : ∀ x ∈ s, commute y x) : + commute y (s.noncomm_prod comm) := begin induction s using quotient.induction_on, simp only [quot_mk_to_coe, noncomm_prod_coe], @@ -219,19 +194,19 @@ variables [monoid β] [monoid γ] given a proof that `*` commutes on all elements `f x` for `x ∈ s`. -/ @[to_additive "Sum of a `s : finset α` mapped with `f : α → β` with `[add_monoid β]`, given a proof that `+` commutes on all elements `f x` for `x ∈ s`."] -def noncomm_prod (s : finset α) (f : α → β) (comm : ∀ (x ∈ s) (y ∈ s), commute (f x) (f y)) : β := -(s.1.map f).noncomm_prod (by simpa [multiset.mem_map, ←finset.mem_def] using comm) +def noncomm_prod (s : finset α) (f : α → β) + (comm : (s : set α).pairwise (λ a b, commute (f a) (f b))) : β := +(s.1.map f).noncomm_prod $ + by { simp_rw multiset.mem_map, rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _, exact comm.of_refl ha hb } @[congr, to_additive] -lemma noncomm_prod_congr - {s₁ s₂ : finset α} {f g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ (x ∈ s₂), f x = g x) - (comm : ∀ (x ∈ s₁) (y ∈ s₁), commute (f x) (f y)) : +lemma noncomm_prod_congr {s₁ s₂ : finset α} {f g : α → β} (h₁ : s₁ = s₂) + (h₂ : ∀ (x ∈ s₂), f x = g x) (comm) : noncomm_prod s₁ f comm = noncomm_prod s₂ g - (λ x hx y hy, h₂ x hx ▸ h₂ y hy ▸ comm x (h₁.symm ▸ hx) y (h₁.symm ▸ hy)) := + (λ x hx y hy h, by { rw [←h₂ _ hx, ←h₂ _ hy], subst h₁, exact comm hx hy h }) := by simp_rw [noncomm_prod, multiset.map_congr (congr_arg _ h₁) h₂] -@[simp, to_additive] lemma noncomm_prod_to_finset [decidable_eq α] (l : list α) (f : α → β) - (comm : ∀ (x ∈ l.to_finset) (y ∈ l.to_finset), commute (f x) (f y)) +@[simp, to_additive] lemma noncomm_prod_to_finset [decidable_eq α] (l : list α) (f : α → β) (comm) (hl : l.nodup) : noncomm_prod l.to_finset f comm = (l.map f).prod := begin @@ -239,43 +214,32 @@ begin simp [noncomm_prod, hl] end -@[simp, to_additive] lemma noncomm_prod_empty (f : α → β) - (h : ∀ (x ∈ (∅ : finset α)) (y ∈ (∅ : finset α)), commute (f x) (f y)) : +@[simp, to_additive] lemma noncomm_prod_empty (f : α → β) (h) : noncomm_prod (∅ : finset α) f h = 1 := rfl @[simp, to_additive] lemma noncomm_prod_insert_of_not_mem [decidable_eq α] (s : finset α) (a : α) - (f : α → β) - (comm : ∀ (x ∈ insert a s) (y ∈ insert a s), commute (f x) (f y)) - (ha : a ∉ s) : - noncomm_prod (insert a s) f comm = f a * noncomm_prod s f - (λ x hx y hy, comm _ (mem_insert_of_mem hx) _ (mem_insert_of_mem hy)) := + (f : α → β) (comm) (ha : a ∉ s) : + noncomm_prod (insert a s) f comm = f a * noncomm_prod s f (comm.mono $ λ _, mem_insert_of_mem) := by simp [insert_val_of_not_mem ha, noncomm_prod] @[to_additive] lemma noncomm_prod_insert_of_not_mem' [decidable_eq α] (s : finset α) (a : α) - (f : α → β) - (comm : ∀ (x ∈ insert a s) (y ∈ insert a s), commute (f x) (f y)) - (ha : a ∉ s) : - noncomm_prod (insert a s) f comm = noncomm_prod s f - (λ x hx y hy, comm _ (mem_insert_of_mem hx) _ (mem_insert_of_mem hy)) * f a := + (f : α → β) (comm) (ha : a ∉ s) : + noncomm_prod (insert a s) f comm = noncomm_prod s f (comm.mono $ λ _, mem_insert_of_mem) * f a := by simp [noncomm_prod, insert_val_of_not_mem ha, multiset.noncomm_prod_cons'] @[simp, to_additive] lemma noncomm_prod_singleton (a : α) (f : α → β) : - noncomm_prod ({a} : finset α) f - (λ x hx y hy, by rw [mem_singleton.mp hx, mem_singleton.mp hy]) = f a := + noncomm_prod ({a} : finset α) f (by { norm_cast, exact set.pairwise_singleton _ _ }) = f a := by simp [noncomm_prod, ←multiset.cons_zero] @[to_additive] -lemma noncomm_prod_map (s : finset α) (f : α → β) - (comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute (f x) (f y)) - {F : Type*} [monoid_hom_class F β γ] (g : F) : +lemma noncomm_prod_map [monoid_hom_class F β γ] (s : finset α) (f : α → β) (comm) (g : F) : g (s.noncomm_prod f comm) = s.noncomm_prod (λ i, g (f i)) - (λ x hx y hy, (comm x hx y hy).map g) := + (λ x hx y hy h, (comm.of_refl hx hy).map g) := by simp [noncomm_prod, multiset.noncomm_prod_map] @[to_additive noncomm_sum_eq_card_nsmul] -lemma noncomm_prod_eq_pow_card (s : finset α) (f : α → β) - (comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute (f x) (f y)) - (m : β) (h : ∀ (x : α), x ∈ s → f x = m) : s.noncomm_prod f comm = m ^ s.card := +lemma noncomm_prod_eq_pow_card (s : finset α) (f : α → β) (comm) (m : β) (h : ∀ x ∈ s, f x = m) : + s.noncomm_prod f comm = m ^ s.card := begin rw [noncomm_prod, multiset.noncomm_prod_eq_pow_card _ _ m], simp only [finset.card_def, multiset.card_map], @@ -283,9 +247,8 @@ begin end @[to_additive noncomm_sum_add_commute] -lemma noncomm_prod_commute (s : finset α) (f : α → β) - (comm : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → commute (f x) (f y)) - (y : β) (h : ∀ (x : α), x ∈ s → commute y (f x)) : commute y (s.noncomm_prod f comm) := +lemma noncomm_prod_commute (s : finset α) (f : α → β) (comm) (y : β) + (h : ∀ x ∈ s, commute y (f x)) : commute y (s.noncomm_prod f comm) := begin apply multiset.noncomm_prod_commute, intro y, @@ -295,7 +258,7 @@ begin end @[to_additive] lemma noncomm_prod_eq_prod {β : Type*} [comm_monoid β] (s : finset α) (f : α → β) : - noncomm_prod s f (λ _ _ _ _, commute.all _ _) = s.prod f := + noncomm_prod s f (λ _ _ _ _ _, commute.all _ _) = s.prod f := begin classical, induction s using finset.induction_on with a s ha IH, @@ -303,16 +266,12 @@ begin { simp [ha, IH] } end -/- The non-commutative version of `finset.prod_union` -/ +/-- The non-commutative version of `finset.prod_union` -/ @[to_additive "The non-commutative version of `finset.sum_union`"] lemma noncomm_prod_union_of_disjoint [decidable_eq α] {s t : finset α} - (h : disjoint s t) (f : α → β) - (comm : ∀ (x ∈ s ∪ t) (y ∈ s ∪ t), commute (f x) (f y)) - (scomm : ∀ (x ∈ s) (y ∈ s), commute (f x) (f y) := - λ _ hx _ hy, comm _ (mem_union_left _ hx) _ (mem_union_left _ hy)) - (tcomm : ∀ (x ∈ t) (y ∈ t), commute (f x) (f y) := - λ _ hx _ hy, comm _ (mem_union_right _ hx) _ (mem_union_right _ hy)) : - noncomm_prod (s ∪ t) f comm = noncomm_prod s f scomm * noncomm_prod t f tcomm := + (h : disjoint s t) (f : α → β) (comm : {x | x ∈ s ∪ t}.pairwise $ λ a b, commute (f a) (f b)) : + noncomm_prod (s ∪ t) f comm = noncomm_prod s f (comm.mono $ coe_subset.2 $ subset_union_left _ _) + * noncomm_prod t f (comm.mono $ coe_subset.2 $ subset_union_right _ _) := begin obtain ⟨sl, sl', rfl⟩ := exists_list_nodup_eq s, obtain ⟨tl, tl', rfl⟩ := exists_list_nodup_eq t, @@ -323,56 +282,46 @@ end @[protected, to_additive] lemma noncomm_prod_mul_distrib_aux {s : finset α} {f : α → β} {g : α → β} - (comm_ff : ∀ (x ∈ s) (y ∈ s), commute (f x) (f y)) - (comm_gg : ∀ (x ∈ s) (y ∈ s), commute (g x) (g y)) - (comm_gf : ∀ (x ∈ s) (y ∈ s), x ≠ y → commute (g x) (f y)) : - (∀ (x ∈ s) (y ∈ s), commute ((f * g) x) ((f * g) y)) := + (comm_ff : (s : set α).pairwise $ λ x y, commute (f x) (f y)) + (comm_gg : (s : set α).pairwise $ λ x y, commute (g x) (g y)) + (comm_gf : (s : set α).pairwise $ λ x y, commute (g x) (f y)) : + (s : set α).pairwise $ λ x y, commute ((f * g) x) ((f * g) y) := begin - intros x hx y hy, - by_cases h : x = y, { subst h }, + intros x hx y hy h, apply commute.mul_left; apply commute.mul_right, - { exact comm_ff x hx y hy }, - { exact (comm_gf y hy x hx (ne.symm h)).symm }, - { exact comm_gf x hx y hy h }, - { exact comm_gg x hx y hy }, + { exact comm_ff.of_refl hx hy }, + { exact (comm_gf hy hx h.symm).symm }, + { exact comm_gf hx hy h }, + { exact comm_gg.of_refl hx hy } end /-- The non-commutative version of `finset.prod_mul_distrib` -/ @[to_additive "The non-commutative version of `finset.sum_add_distrib`"] -lemma noncomm_prod_mul_distrib {s : finset α} (f : α → β) (g : α → β) - (comm_ff : ∀ (x ∈ s) (y ∈ s), commute (f x) (f y)) - (comm_gg : ∀ (x ∈ s) (y ∈ s), commute (g x) (g y)) - (comm_gf : ∀ (x ∈ s) (y ∈ s), x ≠ y → commute (g x) (f y)) : +lemma noncomm_prod_mul_distrib {s : finset α} (f : α → β) (g : α → β) (comm_ff comm_gg comm_gf) : noncomm_prod s (f * g) (noncomm_prod_mul_distrib_aux comm_ff comm_gg comm_gf) = noncomm_prod s f comm_ff * noncomm_prod s g comm_gg := begin classical, induction s using finset.induction_on with x s hnmem ih, { simp, }, - { simp only [finset.noncomm_prod_insert_of_not_mem _ _ _ _ hnmem], - specialize ih - (λ x hx y hy, comm_ff x (mem_insert_of_mem hx) y (mem_insert_of_mem hy)) - (λ x hx y hy, comm_gg x (mem_insert_of_mem hx) y (mem_insert_of_mem hy)) - (λ x hx y hy hne, comm_gf x (mem_insert_of_mem hx) y (mem_insert_of_mem hy) hne), - rw [ih, pi.mul_apply], - simp only [mul_assoc], - congr' 1, - simp only [← mul_assoc], - congr' 1, - apply noncomm_prod_commute, - intros y hy, - have : x ≠ y, by {rintro rfl, contradiction}, - exact comm_gf x (mem_insert_self x s) y (mem_insert_of_mem hy) this, } + simp only [finset.noncomm_prod_insert_of_not_mem _ _ _ _ hnmem], + specialize ih (comm_ff.mono $ λ _, mem_insert_of_mem) (comm_gg.mono $ λ _, mem_insert_of_mem) + (comm_gf.mono $ λ _, mem_insert_of_mem), + rw [ih, pi.mul_apply], + simp only [mul_assoc], + congr' 1, + simp only [← mul_assoc], + congr' 1, + refine noncomm_prod_commute _ _ _ _ (λ y hy, _), + exact comm_gf (mem_insert_self x s) (mem_insert_of_mem hy) (ne_of_mem_of_not_mem hy hnmem).symm, end section finite_pi - -variables {ι : Type*} [fintype ι] [decidable_eq ι] {M : ι → Type*} [∀ i, monoid (M i)] -variables (x : Π i, M i) +variables {M : ι → Type*} [Π i, monoid (M i)] @[to_additive] -lemma noncomm_prod_mul_single : - univ.noncomm_prod (λ i, pi.mul_single i (x i)) (λ i _ j _, pi.mul_single_apply_commute x i j) +lemma noncomm_prod_mul_single [fintype ι] [decidable_eq ι] (x : Π i, M i) : + univ.noncomm_prod (λ i, pi.mul_single i (x i)) (λ i _ j _ _, pi.mul_single_apply_commute x i j) = x := begin ext i, @@ -387,10 +336,11 @@ begin end @[to_additive] -lemma _root_.monoid_hom.pi_ext {f g : (Π i, M i) →* γ} +lemma _root_.monoid_hom.pi_ext [finite ι] [decidable_eq ι] {f g : (Π i, M i) →* γ} (h : ∀ i x, f (pi.mul_single i x) = g (pi.mul_single i x)) : f = g := begin + casesI nonempty_fintype ι, ext x, rw [← noncomm_prod_mul_single x, univ.noncomm_prod_map, univ.noncomm_prod_map], congr' 1 with i, exact h i (x i), diff --git a/src/data/finset/pairwise.lean b/src/data/finset/pairwise.lean index 47e14a48da52e..b9346127ed985 100644 --- a/src/data/finset/pairwise.lean +++ b/src/data/finset/pairwise.lean @@ -70,26 +70,11 @@ variables {β : Type*} [decidable_eq α] {r : α → α → Prop} {l : list α} lemma pairwise_of_coe_to_finset_pairwise (hl : (l.to_finset : set α).pairwise r) (hn : l.nodup) : l.pairwise r := -begin - induction l with hd tl IH, - { simp }, - simp only [set.pairwise_insert, pairwise_cons, to_finset_cons, finset.coe_insert, - finset.mem_coe, mem_to_finset, ne.def, nodup_cons] at hl hn ⊢, - refine ⟨λ x hx, (hl.right x hx _).left, IH hl.left hn.right⟩, - rintro rfl, - exact hn.left hx -end +by { rw coe_to_finset at hl, exact hn.pairwise_of_set_pairwise hl } lemma pairwise_iff_coe_to_finset_pairwise (hn : l.nodup) (hs : symmetric r) : (l.to_finset : set α).pairwise r ↔ l.pairwise r := -begin - refine ⟨λ h, pairwise_of_coe_to_finset_pairwise h hn, λ h, _⟩, - induction l with hd tl IH, - { simp }, - simp only [set.pairwise_insert, to_finset_cons, finset.coe_insert, finset.mem_coe, - mem_to_finset, ne.def, pairwise_cons, nodup_cons] at hn h ⊢, - exact ⟨IH hn.right h.right, λ x hx hne, ⟨h.left _ hx, hs (h.left _ hx)⟩⟩ -end +by { rw [coe_to_finset, hn.pairwise_coe], exact ⟨hs⟩ } lemma pairwise_disjoint_of_coe_to_finset_pairwise_disjoint {α ι} [semilattice_inf α] [order_bot α] [decidable_eq ι] {l : list ι} {f : ι → α} diff --git a/src/data/list/nodup.lean b/src/data/list/nodup.lean index 1a77d853637ca..b15a56f6bd412 100644 --- a/src/data/list/nodup.lean +++ b/src/data/list/nodup.lean @@ -18,7 +18,7 @@ universes u v open nat function -variables {α : Type u} {β : Type v} {l l₁ l₂ : list α} {a b : α} +variables {α : Type u} {β : Type v} {l l₁ l₂ : list α} {r : α → α → Prop} {a b : α} namespace list @@ -352,6 +352,18 @@ lemma nodup.pairwise_of_set_pairwise {l : list α} {r : α → α → Prop} (hl : l.nodup) (h : {x | x ∈ l}.pairwise r) : l.pairwise r := hl.pairwise_of_forall_ne h +@[simp] lemma nodup.pairwise_coe [is_symm α r] (hl : l.nodup) : + {a | a ∈ l}.pairwise r ↔ l.pairwise r := +begin + induction l with a l ih, + { simp }, + rw list.nodup_cons at hl, + have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := + λ b hb, imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm, + simp [set.set_of_or, set.pairwise_insert_of_symmetric (@symm_of _ r _), ih hl.2, and_comm, + forall₂_congr this], +end + end list theorem option.to_list_nodup {α} : ∀ o : option α, o.to_list.nodup diff --git a/src/group_theory/noncomm_pi_coprod.lean b/src/group_theory/noncomm_pi_coprod.lean index 3ed0b04fc1417..0c7b7e4d871e2 100644 --- a/src/group_theory/noncomm_pi_coprod.lean +++ b/src/group_theory/noncomm_pi_coprod.lean @@ -55,7 +55,7 @@ variables {N : ι → Type*} [∀ i, monoid (N i)] variables (ϕ : Π (i : ι), N i →* M) -- We assume that the elements of different morphism commute -variables (hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : N i) (y : N j), commute (ϕ i x) (ϕ j y)) +variables (hcomm : pairwise $ λ i j, ∀ x y, commute (ϕ i x) (ϕ j y)) include hcomm -- We use `f` and `g` to denote elements of `Π (i : ι), N i` @@ -68,8 +68,7 @@ namespace monoid_hom See also `linear_map.lsum` for a linear version without the commutativity assumption."] def noncomm_pi_coprod : (Π (i : ι), N i) →* M := -{ to_fun := λ f, finset.univ.noncomm_prod (λ i, ϕ i (f i)) $ - by { rintros i - j -, by_cases h : i = j, { subst h }, { exact hcomm _ _ h _ _ } }, +{ to_fun := λ f, finset.univ.noncomm_prod (λ i, ϕ i (f i)) $ λ i _ j _ h, hcomm _ _ h _ _, map_one' := by {apply (finset.noncomm_prod_eq_pow_card _ _ _ _ _).trans (one_pow _), simp}, map_mul' := λ f g, begin diff --git a/src/group_theory/perm/cycle/basic.lean b/src/group_theory/perm/cycle/basic.lean index ad15315bd79e6..f7e276194a9c0 100644 --- a/src/group_theory/perm/cycle/basic.lean +++ b/src/group_theory/perm/cycle/basic.lean @@ -929,46 +929,27 @@ end lemma cycle_factors_finset_eq_finset {σ : perm α} {s : finset (perm α)} : σ.cycle_factors_finset = s ↔ (∀ f : perm α, f ∈ s → f.is_cycle) ∧ - (∃ h : (∀ (a ∈ s) (b ∈ s), a ≠ b → disjoint a b), s.noncomm_prod id - (λ a ha b hb, (em (a = b)).by_cases (λ h, h ▸ commute.refl a) - (set.pairwise.mono' (λ _ _, disjoint.commute) h ha hb)) = σ) := + ∃ h : (s : set (perm α)).pairwise disjoint, + s.noncomm_prod id (h.mono' $ λ _ _, disjoint.commute) = σ := begin obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq, - rw cycle_factors_finset_eq_list_to_finset hl, - simp only [noncomm_prod_to_finset, hl, exists_prop, list.mem_to_finset, and.congr_left_iff, - and.congr_right_iff, list.map_id, ne.def], - intros, - exact ⟨list.pairwise.forall disjoint.symmetric, hl.pairwise_of_forall_ne⟩ + simp [cycle_factors_finset_eq_list_to_finset, hl], end -lemma cycle_factors_finset_pairwise_disjoint (p : perm α) (hp : p ∈ cycle_factors_finset f) - (q : perm α) (hq : q ∈ cycle_factors_finset f) (h : p ≠ q) : - disjoint p q := -begin - have : f.cycle_factors_finset = f.cycle_factors_finset := rfl, - obtain ⟨-, hd, -⟩ := cycle_factors_finset_eq_finset.mp this, - exact hd p hp q hq h -end +lemma cycle_factors_finset_pairwise_disjoint : + (cycle_factors_finset f : set (perm α)).pairwise disjoint := +(cycle_factors_finset_eq_finset.mp rfl).2.some -lemma cycle_factors_finset_mem_commute (p : perm α) (hp : p ∈ cycle_factors_finset f) - (q : perm α) (hq : q ∈ cycle_factors_finset f) : - _root_.commute p q := -begin - by_cases h : p = q, - { exact h ▸ commute.refl _ }, - { exact (cycle_factors_finset_pairwise_disjoint _ _ hp _ hq h).commute } -end +lemma cycle_factors_finset_mem_commute : + (cycle_factors_finset f : set (perm α)).pairwise commute := +(cycle_factors_finset_pairwise_disjoint _).mono' $ λ _ _, disjoint.commute /-- The product of cycle factors is equal to the original `f : perm α`. -/ lemma cycle_factors_finset_noncomm_prod - (comm : ∀ (g ∈ f.cycle_factors_finset) (h ∈ f.cycle_factors_finset), - commute (id g) (id h) := cycle_factors_finset_mem_commute f) : - f.cycle_factors_finset.noncomm_prod id (comm) = f := -begin - have : f.cycle_factors_finset = f.cycle_factors_finset := rfl, - obtain ⟨-, hd, hp⟩ := cycle_factors_finset_eq_finset.mp this, - exact hp -end + (comm : (cycle_factors_finset f : set (perm α)).pairwise commute := + cycle_factors_finset_mem_commute f) : + f.cycle_factors_finset.noncomm_prod id comm = f := +(cycle_factors_finset_eq_finset.mp rfl).2.some_spec lemma mem_cycle_factors_finset_iff {f p : perm α} : p ∈ cycle_factors_finset f ↔ p.is_cycle ∧ ∀ (a ∈ p.support), p a = f a := @@ -1056,21 +1037,14 @@ lemma disjoint.cycle_factors_finset_mul_eq_union {f g : perm α} (h : disjoint f cycle_factors_finset (f * g) = cycle_factors_finset f ∪ cycle_factors_finset g := begin rw cycle_factors_finset_eq_finset, - split, - { simp only [mem_cycle_factors_finset_iff, mem_union], - rintro _ (⟨h, -⟩ | ⟨h, -⟩); - exact h }, - { refine ⟨_, _⟩, - { simp_rw mem_union, - rintros x (hx | hx) y (hy | hy) hxy, - { exact cycle_factors_finset_pairwise_disjoint _ _ hx _ hy hxy }, - { exact h.mono (mem_cycle_factors_finset_support_le hx) - (mem_cycle_factors_finset_support_le hy) }, - { exact h.symm.mono (mem_cycle_factors_finset_support_le hx) - (mem_cycle_factors_finset_support_le hy) }, - { exact cycle_factors_finset_pairwise_disjoint _ _ hx _ hy hxy } }, - { rw noncomm_prod_union_of_disjoint h.disjoint_cycle_factors_finset, - rw [cycle_factors_finset_noncomm_prod, cycle_factors_finset_noncomm_prod] } } + refine ⟨_, _, _⟩, + { simp [or_imp_distrib, mem_cycle_factors_finset_iff, forall_swap] }, + { rw [coe_union, set.pairwise_union_of_symmetric disjoint.symmetric], + exact ⟨cycle_factors_finset_pairwise_disjoint _, cycle_factors_finset_pairwise_disjoint _, + λ x hx y hy hxy, h.mono (mem_cycle_factors_finset_support_le hx) + (mem_cycle_factors_finset_support_le hy)⟩ }, + { rw noncomm_prod_union_of_disjoint h.disjoint_cycle_factors_finset, + rw [cycle_factors_finset_noncomm_prod, cycle_factors_finset_noncomm_prod] } end lemma disjoint_mul_inv_of_mem_cycle_factors_finset {f g : perm α} (h : f ∈ cycle_factors_finset g) : diff --git a/src/group_theory/perm/cycle/type.lean b/src/group_theory/perm/cycle/type.lean index b00aac036a120..afc73b7b01826 100644 --- a/src/group_theory/perm/cycle/type.lean +++ b/src/group_theory/perm/cycle/type.lean @@ -47,10 +47,8 @@ lemma cycle_type_def (σ : perm α) : σ.cycle_type = σ.cycle_factors_finset.1.map (finset.card ∘ support) := rfl lemma cycle_type_eq' {σ : perm α} (s : finset (perm α)) - (h1 : ∀ f : perm α, f ∈ s → f.is_cycle) (h2 : ∀ (a ∈ s) (b ∈ s), a ≠ b → disjoint a b) - (h0 : s.noncomm_prod id - (λ a ha b hb, (em (a = b)).by_cases (λ h, h ▸ commute.refl a) - (set.pairwise.mono' (λ _ _, disjoint.commute) h2 ha hb)) = σ) : + (h1 : ∀ f : perm α, f ∈ s → f.is_cycle) (h2 : (s : set (perm α)).pairwise disjoint) + (h0 : s.noncomm_prod id (h2.imp $ λ _ _, disjoint.commute) = σ) : σ.cycle_type = s.1.map (finset.card ∘ support) := begin rw cycle_type_def, diff --git a/src/group_theory/perm/support.lean b/src/group_theory/perm/support.lean index 602a4d84feb29..df00a3cc77659 100644 --- a/src/group_theory/perm/support.lean +++ b/src/group_theory/perm/support.lean @@ -41,6 +41,8 @@ by simp only [disjoint, or.comm, imp_self] lemma disjoint.symmetric : symmetric (@disjoint α) := λ _ _, disjoint.symm +instance : is_symm (perm α) disjoint := ⟨disjoint.symmetric⟩ + lemma disjoint_comm : disjoint f g ↔ disjoint g f := ⟨disjoint.symm, disjoint.symm⟩ diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean index d3974e05b204c..f3f9d7db5d446 100644 --- a/src/group_theory/subgroup/basic.lean +++ b/src/group_theory/subgroup/basic.lean @@ -477,8 +477,7 @@ protected lemma multiset_prod_mem {G} [comm_group G] (K : subgroup G) (g : multi (∀ a ∈ g, a ∈ K) → g.prod ∈ K := multiset_prod_mem g @[to_additive] -lemma multiset_noncomm_prod_mem (K : subgroup G) (g : multiset G) - (comm : ∀ (x ∈ g) (y ∈ g), commute x y) : +lemma multiset_noncomm_prod_mem (K : subgroup G) (g : multiset G) (comm) : (∀ a ∈ g, a ∈ K) → g.noncomm_prod comm ∈ K := K.to_submonoid.multiset_noncomm_prod_mem g comm @@ -492,8 +491,7 @@ protected lemma prod_mem {G : Type*} [comm_group G] (K : subgroup G) prod_mem h @[to_additive] -lemma noncomm_prod_mem (K : subgroup G) - {ι : Type*} {t : finset ι} {f : ι → G} (comm : ∀ (x ∈ t) (y ∈ t), commute (f x) (f y)) : +lemma noncomm_prod_mem (K : subgroup G) {ι : Type*} {t : finset ι} {f : ι → G} (comm) : (∀ c ∈ t, f c ∈ K) → t.noncomm_prod f comm ∈ K := K.to_submonoid.noncomm_prod_mem t f comm @@ -3127,8 +3125,7 @@ disjoint_def'.trans ⟨λ h x y hx hy hxy, generalizes (one direction of) `subgroup.disjoint_iff_mul_eq_one`. -/ @[to_additive "`finset.noncomm_sum` is “injective” in `f` if `f` maps into independent subgroups. This generalizes (one direction of) `add_subgroup.disjoint_iff_add_eq_zero`. "] -lemma eq_one_of_noncomm_prod_eq_one_of_independent {ι : Type*} - (s : finset ι) (f : ι → G) (comm : ∀ (x ∈ s) (y ∈ s), commute (f x) (f y)) +lemma eq_one_of_noncomm_prod_eq_one_of_independent {ι : Type*} (s : finset ι) (f : ι → G) (comm) (K : ι → subgroup G) (hind : complete_lattice.independent K) (hmem : ∀ (x ∈ s), f x ∈ K x) (heq1 : s.noncomm_prod f comm = 1) : ∀ (i ∈ s), f i = 1 := begin @@ -3136,9 +3133,9 @@ begin revert heq1, induction s using finset.induction_on with i s hnmem ih, { simp, }, - { simp only [finset.forall_mem_insert] at comm hmem, - specialize ih (λ x hx, (comm.2 x hx).2) hmem.2, - have hmem_bsupr: s.noncomm_prod f (λ x hx, (comm.2 x hx).2) ∈ ⨆ (i ∈ (s : set ι)), K i, + { have hcomm := comm.mono (finset.coe_subset.2 $ finset.subset_insert _ _), + simp only [finset.forall_mem_insert] at hmem, + have hmem_bsupr: s.noncomm_prod f hcomm ∈ ⨆ (i ∈ (s : set ι)), K i, { refine subgroup.noncomm_prod_mem _ _ _, intros x hx, have : K x ≤ ⨆ (i ∈ (s : set ι)), K i := le_supr₂ x hx, @@ -3148,12 +3145,11 @@ begin have hnmem' : i ∉ (s : set ι), by simpa, obtain ⟨heq1i : f i = 1, heq1S : s.noncomm_prod f _ = 1⟩ := subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_bsupr hnmem') hmem.1 hmem_bsupr heq1, - specialize ih heq1S, intros i h, simp only [finset.mem_insert] at h, rcases h with ⟨rfl | _⟩, { exact heq1i }, - { exact (ih _ h), } } + { exact ih hcomm hmem.2 heq1S _ h } } end end subgroup diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean index d70d06f8b1aa5..8a0e34c4a2119 100644 --- a/src/group_theory/submonoid/membership.lean +++ b/src/group_theory/submonoid/membership.lean @@ -109,8 +109,7 @@ lemma multiset_prod_mem {M} [comm_monoid M] (S : submonoid M) (m : multiset M) by { lift m to multiset S using hm, rw ← coe_multiset_prod, exact m.prod.coe_prop } @[to_additive] -lemma multiset_noncomm_prod_mem (S : submonoid M) (m : multiset M) - (comm : ∀ (x ∈ m) (y ∈ m), commute x y) (h : ∀ (x ∈ m), x ∈ S) : +lemma multiset_noncomm_prod_mem (S : submonoid M) (m : multiset M) (comm) (h : ∀ (x ∈ m), x ∈ S) : m.noncomm_prod comm ∈ S := begin induction m using quotient.induction_on with l, @@ -128,8 +127,8 @@ lemma prod_mem {M : Type*} [comm_monoid M] (S : submonoid M) S.multiset_prod_mem (t.1.map f) $ λ x hx, let ⟨i, hi, hix⟩ := multiset.mem_map.1 hx in hix ▸ h i hi @[to_additive] -lemma noncomm_prod_mem (S : submonoid M) {ι : Type*} (t : finset ι) (f : ι → M) - (comm : ∀ (x ∈ t) (y ∈ t), commute (f x) (f y)) (h : ∀ c ∈ t, f c ∈ S) : +lemma noncomm_prod_mem (S : submonoid M) {ι : Type*} (t : finset ι) (f : ι → M) (comm) + (h : ∀ c ∈ t, f c ∈ S) : t.noncomm_prod f comm ∈ S := begin apply multiset_noncomm_prod_mem,