Theorems · Theorem · group theory

Equiv.Perm.SameCycle.exists_pow_eq

∀ {α : Type u_2} {x y : α} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α),
  f.SameCycle x y → ∃ i, 0 < i ∧ i ≤ (f.cycleOf x).support.card + 1 ∧ (f ^ i) x = y

Defined in

Mathlib.GroupTheory.Perm.Cycle.Factors

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype