Theorems · Theorem · group theory

Equiv.Perm.Basis.sameCycle

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis) {x : α}
  (hx : g.cycleOf x ∈ g.cycleFactorsFinset), g.SameCycle (a ⟨g.cycleOf x, hx⟩) x

Defined in

Mathlib.GroupTheory.Perm.Centralizer

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype