English
A variant induction principle: using right-multiplication by swaps, the motive propagates similarly to swap_induction_on.
Русский
Вариант принципа индукции: переход по правому умножению на транспозицию распространяет свойство аналогично swap_induction_on.
LaTeX
$$$ [Finite\\ α] {motive : Perm α \\to Prop} (f : Perm α) (one : motive 1) (mul_swap : \\forall f x y, x \\neq y \\to motive f \\\\to motive (f * swap x y)) : motive f $$$
Lean4
/-- Like `swap_induction_on`, but with the composition on the right of `f`.
An induction principle for permutations. If `motive` holds for the identity permutation, and
is preserved under composition with a non-trivial swap, then `motive` holds for all permutations. -/
@[elab_as_elim]
theorem swap_induction_on' [Finite α] {motive : Perm α → Prop} (f : Perm α) (one : motive 1)
(mul_swap : ∀ f x y, x ≠ y → motive f → motive (f * swap x y)) : motive f :=
inv_inv f ▸ swap_induction_on f⁻¹ one fun f => mul_swap f⁻¹
