feat(data/finset/noncomm_prod): add noncomm_prod_commute (#12521)

adding `list.prod_commute`, `multiset.noncomm_prod_commute` and
`finset.noncomm_prod_commute`.

src/data/finset/noncomm_prod.lean

@@ -170,6 +170,16 @@ begin
   simp
 end
 
+@[to_additive]
+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) :=
+begin
+  induction s using quotient.induction_on,
+  simp only [quot_mk_to_coe, noncomm_prod_coe],
+  exact list.prod_commute _ _ h,
+end
+
 end multiset
 
 namespace finset
@@ -225,6 +235,18 @@ by simp [noncomm_prod, insert_val_of_not_mem ha, multiset.noncomm_prod_cons']
     (λ x hx y hy, by rw [mem_singleton.mp hx, mem_singleton.mp hy]) = f a :=
 by simp [noncomm_prod, multiset.singleton_eq_cons]
 
+@[to_additive]
+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) :=
+begin
+  apply multiset.noncomm_prod_commute,
+  intro y,
+  rw multiset.mem_map,
+  rintros ⟨x, ⟨hx, rfl⟩⟩,
+  exact h x hx,
+end
+
 @[to_additive] lemma noncomm_prod_eq_prod {β : Type*} [comm_monoid β] (s : finset α) (f : α → β) :
   noncomm_prod s f (λ _ _ _ _, commute.all _ _) = s.prod f :=
 begin

src/data/list/prod_monoid.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 -/
 import data.list.big_operators
+import algebra.group.commute
 
 /-!
 # Products / sums of lists of terms of a monoid
@@ -32,9 +33,19 @@ lemma prod_le_of_forall_le [ordered_comm_monoid α] (l : list α) (n : α) (h :
 begin
   induction l with y l IH,
   { simp },
-  { specialize IH (λ x hx, h x (mem_cons_of_mem _ hx)),
-    have hy : y ≤ n := h y (mem_cons_self _ _),
-    simpa [pow_succ] using mul_le_mul' hy IH }
+  { rw list.ball_cons at h,
+    simpa [pow_succ] using mul_le_mul' h.1 (IH h.2) }
+end
+
+@[to_additive]
+lemma prod_commute [monoid α] (l : list α)
+  (y : α) (h : ∀ (x ∈ l), commute y x) : commute y l.prod :=
+begin
+  induction l with y l IH,
+  { simp },
+  { rw list.ball_cons at h,
+    rw list.prod_cons,
+    exact commute.mul_right h.1 (IH h.2), }
 end
 
 end list