Theorems · Theorem · group theory

Equiv.Perm.pairwise_commute_of_mem_zpowers

∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α),
  Pairwise fun i j => ∀ (x y : Equiv.Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Commute x y

Defined in

Mathlib.GroupTheory.Perm.Cycle.Factors

Cited by

7 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype