Theorems · Theorem · group theory

Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff

∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {g c : Equiv.Perm α} {s : Finset α}
  (hg : ∀ (x : α), g x ∈ s ↔ x ∈ s) (hc : c.support ⊆ s) (n : ℤ),
  c ^ n = Equiv.Perm.ofSubtype (g.subtypePerm hg) ↔ c.subtypePerm ⋯ ^ n = g.subtypePerm hg

Defined in

Mathlib.GroupTheory.Perm.Cycle.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq