feat(Algebra/Group): lemmas about Commute (#8756)

Mathlib/Algebra/Group/Pi.lean

@@ -545,6 +545,26 @@ theorem Pi.single_mul_right [∀ i, MulZeroClass <| f i] (a : f i) :
   funext fun _ => Pi.single_mul_right_apply _ _ _ _
 #align pi.single_mul_right Pi.single_mul_right
 
+section
+variable [∀ i, Mul <| f i]
+
+@[to_additive]
+theorem SemiconjBy.pi {x y z : ∀ i, f i} (h : ∀ i, SemiconjBy (x i) (y i) (z i)) :
+    SemiconjBy x y z :=
+  funext h
+
+@[to_additive]
+theorem Pi.semiconjBy_iff {x y z : ∀ i, f i} :
+    SemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i) := Function.funext_iff
+
+@[to_additive]
+theorem Commute.pi {x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y := .pi h
+
+@[to_additive]
+theorem Pi.commute_iff {x y : ∀ i, f i} : Commute x y ↔ ∀ i, Commute (x i) (y i) := semiconjBy_iff
+
+end
+
 /-- The injection into a pi group at different indices commutes.
 
 For injections of commuting elements at the same index, see `Commute.map` -/

Mathlib/Algebra/Group/Prod.lean

@@ -301,6 +301,26 @@ instance instCommGroup [CommGroup G] [CommGroup H] : CommGroup (G × H) :=
 
 end Prod
 
+section
+variable [Mul M] [Mul N]
+
+@[to_additive AddSemiconjBy.prod]
+theorem SemiconjBy.prod {x y z : M × N}
+    (hm : SemiconjBy x.1 y.1 z.1) (hn : SemiconjBy x.2 y.2 z.2) : SemiconjBy x y z :=
+  Prod.ext hm hn
+
+theorem Prod.semiconjBy_iff {x y z : M × N} :
+    SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2 := ext_iff
+
+@[to_additive AddCommute.prod]
+theorem Commute.prod {x y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y :=
+  .prod hm hn
+
+theorem Prod.commute_iff {x y : M × N} :
+    Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2 := semiconjBy_iff
+
+end
+
 namespace MulHom
 
 section Prod