Theorems · Theorem · group theory

Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) {x : α} {c : ↥g.cycleFactorsFinset},
  x ∈ (↑c).support → ∀ {m : ℤ}, (g ^ m) (a c) = x → a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Defined in

Mathlib.GroupTheory.Perm.Centralizer

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype