chore(Perm/Basic): generalize swap_smul_involutive (#9180)

Generalize `Equiv.Perm.ModSumCongr.swap_smul_involutive` to any action of `Equiv.Perm _`, move it to `Perm/Basic`.

Mathlib/GroupTheory/Perm/Basic.lean

@@ -535,13 +535,20 @@ theorem swap_apply_apply (f : Perm α) (x y : α) : swap (f x) (f y) = f * swap
   rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]
 #align equiv.swap_apply_apply Equiv.swap_apply_apply
 
+@[simp]
+theorem swap_smul_self_smul [MulAction (Perm α) β] (i j : α) (x : β) :
+    swap i j • swap i j • x = x := by simp [smul_smul]
+
+theorem swap_smul_involutive [MulAction (Perm α) β] (i j : α) :
+    Function.Involutive (swap i j • · : β → β) := swap_smul_self_smul i j
+
 /-- Left-multiplying a permutation with `swap i j` twice gives the original permutation.
 
   This specialization of `swap_mul_self` is useful when using cosets of permutations.
 -/
 @[simp]
-theorem swap_mul_self_mul (i j : α) (σ : Perm α) : Equiv.swap i j * (Equiv.swap i j * σ) = σ := by
-  rw [← mul_assoc, swap_mul_self, one_mul]
+theorem swap_mul_self_mul (i j : α) (σ : Perm α) : Equiv.swap i j * (Equiv.swap i j * σ) = σ :=
+  swap_smul_self_smul i j σ
 #align equiv.swap_mul_self_mul Equiv.swap_mul_self_mul
 
 /-- Right-multiplying a permutation with `swap i j` twice gives the original permutation.

Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

@@ -32,12 +32,7 @@ abbrev ModSumCongr (α β : Type*) :=
   _ ⧸ (Equiv.Perm.sumCongrHom α β).range
 #align equiv.perm.mod_sum_congr Equiv.Perm.ModSumCongr
 
-theorem ModSumCongr.swap_smul_involutive {α β : Type*} [DecidableEq (Sum α β)] (i j : Sum α β) :
-    Function.Involutive (SMul.smul (Equiv.swap i j) : ModSumCongr α β → ModSumCongr α β) :=
-  fun σ => by
-    refine Quotient.inductionOn' σ fun σ => ?_
-    exact _root_.congr_arg Quotient.mk'' (Equiv.swap_mul_involutive i j σ)
-#align equiv.perm.mod_sum_congr.swap_smul_involutive Equiv.Perm.ModSumCongr.swap_smul_involutive
+#align equiv.perm.mod_sum_congr.swap_smul_involutive Equiv.swap_smul_involutive
 
 end Equiv.Perm
 
@@ -171,7 +166,7 @@ def domCoprod (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N
           (fun σ _ => domCoprod.summand_add_swap_smul_eq_zero a b σ hv hij)
           (fun σ _ => mt <| domCoprod.summand_eq_zero_of_smul_invariant a b σ hv hij)
           (fun σ _ => Finset.mem_univ _) fun σ _ =>
-          Equiv.Perm.ModSumCongr.swap_smul_involutive i j σ }
+          Equiv.swap_smul_involutive i j σ }
 #align alternating_map.dom_coprod AlternatingMap.domCoprod
 #align alternating_map.dom_coprod_apply AlternatingMap.domCoprod_apply