Theorems · Theorem · group theory

Equiv.Perm.Disjoint.cycleType_noncommProd

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {ι : Type u_2} {k : ι → Equiv.Perm α} {s : Finset ι}
  (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
  (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
  (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

Defined in

Mathlib.GroupTheory.Perm.Cycle.Type

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq