feat(group_theory/group_action): add `commute.smul_{left,right}[_iff]…

…` lemmas (#13003)

`(r • a) * b = b * (r • a)` follows trivially from `smul_mul_assoc` and `mul_smul_comm`

src/group_theory/group_action/defs.lean

@@ -46,7 +46,7 @@ group action
 
 variables {M N G A B α β γ : Type*}
 
-open function
+open function (injective surjective)
 
 /-!
 ### Faithful actions
@@ -383,6 +383,16 @@ lemma smul_mul_smul [has_mul α] (r s : M) (x y : α)
   (r • x) * (s • y) = (r * s) • (x * y) :=
 by rw [smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
 
+lemma commute.smul_right [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]
+  {a b : α} (h : commute a b) (r : M) :
+  commute a (r • b) :=
+(mul_smul_comm _ _ _).trans ((congr_arg _ h).trans $ (smul_mul_assoc _ _ _).symm)
+
+lemma commute.smul_left [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α]
+  {a b : α} (h : commute a b) (r : M) :
+  commute (r • a) b :=
+(h.symm.smul_right r).symm
+
 end
 
 namespace mul_action

src/group_theory/group_action/group.lean

@@ -94,6 +94,16 @@ lemma smul_zpow [group β] [smul_comm_class α β β] [is_scalar_tower α β β]
   (c • x) ^ p = c ^ p • x ^ p :=
 by { cases p; simp [smul_pow, smul_inv] }
 
+@[simp] lemma commute.smul_right_iff [has_mul β] [smul_comm_class α β β] [is_scalar_tower α β β]
+  {a b : β} (r : α) :
+  commute a (r • b) ↔ commute a b :=
+⟨λ h, inv_smul_smul r b ▸ h.smul_right r⁻¹, λ h, h.smul_right r⟩
+
+@[simp] lemma commute.smul_left_iff [has_mul β] [smul_comm_class α β β] [is_scalar_tower α β β]
+  {a b : β} (r : α) :
+  commute (r • a) b ↔ commute a b :=
+by rw [commute.symm_iff, commute.smul_right_iff, commute.symm_iff]
+
 @[to_additive] protected lemma mul_action.bijective (g : α) : function.bijective (λ b : β, g • b) :=
 (mul_action.to_perm g).bijective
 
@@ -134,6 +144,16 @@ lemma inv_smul_eq_iff₀ {a : α} (ha : a ≠ 0) {x y : β} : a⁻¹ • x = y 
 lemma eq_inv_smul_iff₀ {a : α} (ha : a ≠ 0) {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
 (mul_action.to_perm (units.mk0 a ha)).eq_symm_apply
 
+@[simp] lemma commute.smul_right_iff₀ [has_mul β] [smul_comm_class α β β] [is_scalar_tower α β β]
+  {a b : β} {c : α} (hc : c ≠ 0) :
+  commute a (c • b) ↔ commute a b :=
+commute.smul_right_iff (units.mk0 c hc)
+
+@[simp] lemma commute.smul_left_iff₀ [has_mul β] [smul_comm_class α β β] [is_scalar_tower α β β]
+  {a b : β} {c : α} (hc : c ≠ 0) :
+  commute (c • a) b ↔ commute a b :=
+commute.smul_left_iff (units.mk0 c hc)
+
 end gwz
 
 end mul_action