Theorems · Theorem · group theory

Equiv.Perm.cycleType_extendDomain

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {β : Type u_2} [inst_2 : Fintype β]
  [inst_3 : DecidableEq β] {p : β → Prop} [inst_4 : DecidablePred p] (f : α ≃ Subtype p) {g : Equiv.Perm α},
  (g.extendDomain f).cycleType = g.cycleType

Defined in

Mathlib.GroupTheory.Perm.Cycle.Type

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqFintypeDecidableEqDecidablePred