Theorems · Theorem · group theory

Equiv.Perm.swap_induction_on

∀ {α : Type u} [inst : DecidableEq α] [Finite α] {motive : Equiv.Perm α → Prop} (f : Equiv.Perm α),
  motive 1 → (∀ (f : Equiv.Perm α) (x y : α), x ≠ y → motive f → motive (Equiv.swap x y * f)) → motive 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.

Defined in

Mathlib.GroupTheory.Perm.Sign

Cited by

5 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFinite