chore(group_theory/perm/basic): Add missing lemmas (#5320)

These lemmas existed for left multiplication but not right multiplication

src/group_theory/perm/basic.lean

@@ -104,24 +104,42 @@ end
 lemma mul_swap_eq_swap_mul (f : perm α) (x y : α) : f * swap x y = swap (f x) (f y) * f :=
 by rw [swap_mul_eq_mul_swap, perm.inv_apply_self, perm.inv_apply_self]
 
-/-- Multiplying a permutation with `swap i j` twice gives the original permutation.
+/-- 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]
 lemma swap_mul_self_mul (i j : α) (σ : perm α) : equiv.swap i j * (equiv.swap i j * σ) = σ :=
 by rw [←mul_assoc, swap_mul_self, one_mul]
 
+/-- Right-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]
+lemma mul_swap_mul_self (i j : α) (σ : perm α) : (σ * equiv.swap i j) * equiv.swap i j = σ :=
+by rw [mul_assoc, swap_mul_self, mul_one]
+
 /-- A stronger version of `mul_right_injective` -/
 @[simp]
 lemma swap_mul_involutive (i j : α) : function.involutive ((*) (equiv.swap i j)) :=
 swap_mul_self_mul i j
 
+/-- A stronger version of `mul_left_injective` -/
+@[simp]
+lemma mul_swap_involutive (i j : α) : function.involutive (* (equiv.swap i j)) :=
+mul_swap_mul_self i j
+
 lemma swap_mul_eq_iff {i j : α} {σ : perm α} : swap i j * σ = σ ↔ i = j :=
 ⟨(assume h, have swap_id : swap i j = 1 := mul_right_cancel (trans h (one_mul σ).symm),
   by {rw [←swap_apply_right i j, swap_id], refl}),
 (assume h, by erw [h, swap_self, one_mul])⟩
 
+lemma mul_swap_eq_iff {i j : α} {σ : perm α} : σ * swap i j = σ ↔ i = j :=
+⟨(assume h, have swap_id : swap i j = 1 := mul_left_cancel (trans h (one_mul σ).symm),
+  by {rw [←swap_apply_right i j, swap_id], refl}),
+(assume h, by erw [h, swap_self, mul_one])⟩
+
 lemma swap_mul_swap_mul_swap {x y z : α} (hwz: x ≠ y) (hxz : x ≠ z) :
   swap y z * swap x y * swap y z = swap z x :=
 equiv.ext $ λ n, by { simp only [swap_apply_def, perm.mul_apply], split_ifs; cc }

src/linear_algebra/determinant.lean

@@ -67,9 +67,9 @@ begin
           (λ _ _ _ _ h, (swap i j).injective h)
           (λ b _, ⟨swap i j b, mem_univ _, by simp⟩),
       by simp [sign_mul, this, sign_swap hij, prod_mul_distrib])
-    (λ σ _ _ h, hij (σ.injective $ by conv {to_lhs, rw ← h}; simp))
+    (λ σ _ _, (not_congr mul_swap_eq_iff).mpr hij)
     (λ _ _, mem_univ _)
-    (λ _ _, equiv.ext $ by simp)
+    (λ σ _, mul_swap_involutive i j σ)
 end
 
 @[simp] lemma det_mul (M N : matrix n n R) : det (M ⬝ N) = det M * det N :=