Theorems · Definition · group theory

Equiv.Perm.Basis.toCentralizer

{α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] →
      {g : Equiv.Perm α} → g.Basis → ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g) →* ↥(Subgroup.centralizer {g})

Given a : Equiv.Perm.Basis g, we define a right inverse of Equiv.Perm.OnCycleFactors.toPermHom, on range_toPermHom' g

Defined in

Mathlib.GroupTheory.Perm.Centralizer

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype