Theorems · Theorem · group theory

mem_closure_isSwap

∀ {α : Type u_2} [inst : DecidableEq α] {S : Set (Equiv.Perm α)},
  (∀ f ∈ S, f.IsSwap) →
    ∀ {f : Equiv.Perm α},
      f ∈ Subgroup.closure S ↔
        (MulAction.fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), f x ∈ MulAction.orbit (↥(Subgroup.closure S)) x

If a subgroup is generated by transpositions, then a permutation f lies in the subgroup if and only if f has finite support and f x always lies in the same orbit as x.

Defined in

Mathlib.GroupTheory.Perm.ClosureSwap

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq