Theorems · Theorem · group theory

Equiv.Perm.Basis.ofPermHomFun_commute_zpow_apply

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

Defined in: Mathlib.GroupTheory.Perm.Centralizer
Cited by: 2 results in Mathlib
Foundations: Depth 102 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.

Cites20

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

DFunLike.coestatement and proof · cited by 62,936
Finsetstatement · cited by 13,712
Fintypestatement and proof · cited by 7,736
Subgroupstatement · cited by 3,593
add_commproof · cited by 1,535
Equiv.Permstatement and proof · cited by 1,375
Equiv.Perm.supportproof · cited by 230
Equiv.Perm.cycleFactorsFinsetstatement and proof · cited by 96
Function.fixedPointsproof · cited by 90
zpow_addproof · cited by 40
Equiv.Perm.mul_applyproof · cited by 38
Equiv.Perm.Basisstatement and proof · cited by 25

Cited by2

Results whose statement or proof uses this declaration.

Equiv.Perm.Basis.toCentralizer_equivariantproof · cited by 1
Equiv.Perm.Basis.ofPermHom_mem_centralizerproof · cited by 0