Theorems · Theorem · group theory

Equiv.Perm.mem_list_cycles_iff

∀ {α : Type u_4} [Finite α] {l : List (Equiv.Perm α)},
  (∀ σ ∈ l, σ.IsCycle) →
    List.Pairwise Equiv.Perm.Disjoint l → ∀ {σ : Equiv.Perm α}, σ ∈ l ↔ σ.IsCycle ∧ ∀ (a : α), σ a ≠ a → σ a = l.prod a

Defined in

Mathlib.GroupTheory.Perm.Cycle.Factors

Cited by

2 results in Mathlib

Foundations

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

Assumes

Finite