Theorems · Theorem · group theory

Equiv.Perm.mem_cycleType_iff

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {n : ℕ} {σ : Equiv.Perm α},
  n ∈ σ.cycleType ↔ ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ c.support.card = n

Defined in

Mathlib.GroupTheory.Perm.Cycle.Type

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq