feat(algebra/big_operators): add commute.*_sum_{left,right} lemmas (#13035)

This moves the existing `prod_commute` lemmas into the `commute` namespace for discoverabiliy, and adds the swapped variants.

This also fixes an issue where lemmas about `add_commute` were misnamed using `commute`.

Author: eric-wieser

src/algebra/big_operators/basic.lean

@@ -1305,6 +1305,19 @@ begin
   simp [finset.sum_range_succ', add_comm]
 end
 
+lemma _root_.commute.sum_right [non_unital_non_assoc_semiring β] (s : finset α)
+  (f : α → β) (b : β) (h : ∀ i ∈ s, commute b (f i)) :
+  commute b (∑ i in s, f i) :=
+commute.multiset_sum_right _ _ $ λ b hb, begin
+  obtain ⟨i, hi, rfl⟩ := multiset.mem_map.mp hb,
+  exact h _ hi
+end
+
+lemma _root_.commute.sum_left [non_unital_non_assoc_semiring β] (s : finset α)
+  (f : α → β) (b : β) (h : ∀ i ∈ s, commute (f i) b) :
+  commute (∑ i in s, f i) b :=
+(commute.sum_right _ _ _ $ λ i hi, (h _ hi).symm).symm
+
 section opposite
 
 open mul_opposite

src/algebra/big_operators/multiset.lean

@@ -234,7 +234,19 @@ by { convert (m.map f).prod_hom (zpow_group_hom₀ _ : α →* α), rw map_map,
 end comm_group_with_zero
 
 section semiring
-variables [semiring α] {a : α} {s : multiset ι} {f : ι → α}
+variables [non_unital_non_assoc_semiring α] {a : α} {s : multiset ι} {f : ι → α}
+
+lemma _root_.commute.multiset_sum_right (s : multiset α) (a : α) (h : ∀ b ∈ s, commute a b) :
+  commute a s.sum :=
+begin
+  induction s using quotient.induction_on,
+  rw [quot_mk_to_coe, coe_sum],
+  exact commute.list_sum_right _ _ h,
+end
+
+lemma _root_.commute.multiset_sum_left (s : multiset α) (b : α) (h : ∀ a ∈ s, commute a b) :
+  commute s.sum b :=
+(commute.multiset_sum_right _ _ $ λ a ha, (h _ ha).symm).symm
 
 lemma sum_map_mul_left : sum (s.map (λ i, a * f i)) = a * sum (s.map f) :=
 multiset.induction_on s (by simp) (λ i s ih, by simp [ih, mul_add])

src/data/finset/noncomm_prod.lean

@@ -199,14 +199,14 @@ begin
   simp
 end
 
-@[to_additive]
+@[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) :=
 begin
   induction s using quotient.induction_on,
   simp only [quot_mk_to_coe, noncomm_prod_coe],
-  exact list.prod_commute _ _ h,
+  exact commute.list_prod_right _ _ h,
 end
 
 end multiset
@@ -282,7 +282,7 @@ begin
   simpa using h,
 end
 
-@[to_additive]
+@[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) :=

src/data/list/big_operators.lean

@@ -161,7 +161,8 @@ lemma head_mul_tail_prod_of_ne_nil [inhabited M] (l : list M) (h : l ≠ []) :
 by cases l; [contradiction, simp]
 
 @[to_additive]
-lemma prod_commute (l : list M) (y : M) (h : ∀ (x ∈ l), commute y x) : commute y l.prod :=
+lemma _root_.commute.list_prod_right (l : list M) (y : M) (h : ∀ (x ∈ l), commute y x) :
+  commute y l.prod :=
 begin
   induction l with z l IH,
   { simp },
@@ -170,6 +171,26 @@ begin
     exact commute.mul_right h.1 (IH h.2), }
 end
 
+@[to_additive]
+lemma _root_.commute.list_prod_left (l : list M) (y : M) (h : ∀ (x ∈ l), commute x y) :
+  commute l.prod y  :=
+(commute.list_prod_right _ _ $ λ x hx, (h _ hx).symm).symm
+
+lemma _root_.commute.list_sum_right [non_unital_non_assoc_semiring R] (a : R) (l : list R)
+  (h : ∀ b ∈ l, commute a b) :
+  commute a l.sum :=
+begin
+  induction l with x xs ih,
+  { exact commute.zero_right _, },
+  { rw sum_cons,
+    exact (h _ $ mem_cons_self _ _).add_right (ih $ λ j hj, h _ $ mem_cons_of_mem _ hj) }
+end
+
+lemma _root_.commute.list_sum_left [non_unital_non_assoc_semiring R] (b : R) (l : list R)
+  (h : ∀ a ∈ l, commute a b) :
+  commute l.sum b :=
+(commute.list_sum_right _ _ $ λ x hx, (h _ hx).symm).symm
+
 @[to_additive sum_le_sum] lemma prod_le_prod' [preorder M]
   [covariant_class M M (function.swap (*)) (≤)] [covariant_class M M (*) (≤)]
   {l : list ι} {f g : ι → M} (h : ∀ i ∈ l, f i ≤ g i) :