Theorems · Theorem · group theory

Equiv.Perm.cycle_is_cycleOf

∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f c : Equiv.Perm α} {a : α},
  a ∈ c.support → c ∈ f.cycleFactorsFinset → c = f.cycleOf a

If c is a cycle, a ∈ c.support and c is a cycle of f, then c = f.cycleOf a

Defined in

Mathlib.GroupTheory.Perm.Cycle.Factors

Cited by

4 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype