Theorems · Theorem · group theory

Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α) (k : ↥(Subgroup.centralizer {g})),
  k ∈ (Equiv.Perm.OnCycleFactors.toPermHom g).ker ↔ ∀ c ∈ g.cycleFactorsFinset, Commute (↑k) c

k : Subgroup.centralizer {g} belongs to the kernel of toPermHom g iff it commutes with each cycle of g

Defined in

Mathlib.GroupTheory.Perm.Centralizer

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype