From 1eaf499975153f102a132a5d9b8d06f5208b5fc8 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 12 Mar 2022 04:22:20 +0000
Subject: [PATCH] feat(group_theory/subgroup/basic):
 {multiset_,}noncomm_prod_mem (#12523)

and same for submonoids.
---
 src/group_theory/subgroup/basic.lean       | 13 ++++++++++++
 src/group_theory/submonoid/membership.lean | 23 ++++++++++++++++++++++
 2 files changed, 36 insertions(+)

diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 6e67eb8e1ab5e..6220cf815914f 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -292,6 +292,12 @@ is in the `add_subgroup`."]
 lemma multiset_prod_mem {G} [comm_group G] (K : subgroup G) (g : multiset G) :
   (∀ a ∈ g, a ∈ K) → g.prod ∈ K := K.to_submonoid.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) :
+  (∀ a ∈ g, a ∈ K) → g.noncomm_prod comm ∈ K :=
+K.to_submonoid.multiset_noncomm_prod_mem g comm
+
 /-- Product of elements of a subgroup of a `comm_group` indexed by a `finset` is in the
     subgroup. -/
 @[to_additive "Sum of elements in an `add_subgroup` of an `add_comm_group` indexed by a `finset`
@@ -301,6 +307,13 @@ lemma prod_mem {G : Type*} [comm_group G] (K : subgroup G)
   ∏ c in t, f c ∈ K :=
 K.to_submonoid.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)) :
+  (∀ c ∈ t, f c ∈ K) → t.noncomm_prod f comm ∈ K :=
+K.to_submonoid.noncomm_prod_mem t f comm
+
+
 @[to_additive add_subgroup.nsmul_mem]
 lemma pow_mem {x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K := K.to_submonoid.pow_mem hx
 
diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean
index 9aef020b84be2..7a4afcc18b3d9 100644
--- a/src/group_theory/submonoid/membership.lean
+++ b/src/group_theory/submonoid/membership.lean
@@ -7,6 +7,7 @@ Amelia Livingston, Yury Kudryashov
 import group_theory.submonoid.operations
 import algebra.big_operators.basic
 import algebra.free_monoid
+import data.finset.noncomm_prod
 
 /-!
 # Submonoids: membership criteria
@@ -65,6 +66,16 @@ lemma multiset_prod_mem {M} [comm_monoid M] (S : submonoid M) (m : multiset M)
   (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S :=
 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) :
+  m.noncomm_prod comm ∈ S :=
+begin
+  induction m using quotient.induction_on with l,
+  simp only [multiset.quot_mk_to_coe, multiset.noncomm_prod_coe],
+  exact submonoid.list_prod_mem _ h,
+end
+
 /-- Product of elements of a submonoid of a `comm_monoid` indexed by a `finset` is in the
     submonoid. -/
 @[to_additive "Sum of elements in an `add_submonoid` of an `add_comm_monoid` indexed by a `finset`
@@ -74,6 +85,18 @@ lemma prod_mem {M : Type*} [comm_monoid M] (S : submonoid M)
   ∏ c in t, f c ∈ S :=
 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) :
+  t.noncomm_prod f comm ∈ S :=
+begin
+  apply multiset_noncomm_prod_mem,
+  intro y,
+  rw multiset.mem_map,
+  rintros ⟨x, ⟨hx, rfl⟩⟩,
+  exact h x hx,
+end
+
 end assoc
 
 section non_assoc