feat(group_theory/perm/sign): Add swap_induction_on' (#5092)

This also adds a docstring for swap_induction_on

src/group_theory/perm/sign.lean

@@ -247,6 +247,8 @@ quotient.rec_on_subsingleton (@univ α _).1
 (λ l h, trunc.mk (swap_factors_aux l f h))
 (show ∀ x, f x ≠ x → x ∈ (@univ α _).1, from λ _ _, mem_univ _)
 
+/-- An induction principle for permutations. If `P` holds for the identity permutation, and
+is preserved under composition with a non-trivial swap, then `P` holds for all permutations. -/
 @[elab_as_eliminator] lemma swap_induction_on [fintype α] {P : perm α → Prop} (f : perm α) :
   P 1 → (∀ f x y, x ≠ y → P f → P (swap x y * f)) → P f :=
 begin
@@ -259,6 +261,14 @@ begin
     exact hmul_swap _ _ _ hxy.1 (ih _ ⟨rfl, λ v hv, hl.2 _ (list.mem_cons_of_mem _ hv)⟩ h1 hmul_swap) }
 end
 
+/-- Like `swap_induction_on`, but with the composition on the right of `f`.
+
+An induction principle for permutations. If `P` holds for the identity permutation, and
+is preserved under composition with a non-trivial swap, then `P` holds for all permutations. -/
+@[elab_as_eliminator] lemma swap_induction_on' [fintype α] {P : perm α → Prop} (f : perm α) :
+  P 1 → (∀ f x y, x ≠ y → P f → P (f * swap x y)) → P f :=
+λ h1 IH, inv_inv f ▸ swap_induction_on f⁻¹ h1 (λ f, IH f⁻¹)
+
 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, mul_apply]; split_ifs; cc