Theorems · Definition · group theory

Equiv.Perm.Basis.ofPermHomFun

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

The function that will provide a right inverse toCentralizer to toPermHom

Defined in: Mathlib.GroupTheory.Perm.Centralizer
Cited by: 9 results in Mathlib
Foundations: Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Finsetstatement · cited by 13,712
Fintypestatement and proof · cited by 7,736
Subgroupstatement · cited by 3,593
Equiv.Permstatement and proof · cited by 1,375
Nat.findproof · cited by 139
Equiv.Perm.cycleFactorsFinsetstatement and proof · cited by 96
Equiv.Perm.cycleOfproof · cited by 59
Equiv.Perm.Basisstatement and proof · cited by 25
Equiv.Perm.OnCycleFactors.range_toPermHom'statement and proof · cited by 16

Cited by10

Results whose statement or proof uses this declaration.

Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_memstatement and proof · cited by 5
Equiv.Perm.Basis.ofPermHomFun_apply_of_mem_fixedPointsstatement · cited by 5
Equiv.Perm.Basis.ofPermHomproof · cited by 4
Equiv.Perm.Basis.ofPermHomFun_commute_zpow_applystatement and proof · cited by 2
Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iffstatement · cited by 1
Equiv.Perm.Basis.toCentralizer_equivariantproof · cited by 1
Equiv.Perm.Basis.ofPermHomFun_mulstatement and proof · cited by 0
Equiv.Perm.Basis.ofPermHomFun_onestatement · cited by 0
Equiv.Perm.Basis.ofPermHom_applystatement · cited by 0
Equiv.Perm.Basis.toCentralizer_applystatement · cited by 0