# Documentation

Mathlib.GroupTheory.Perm.Cycle.Basic

# Cyclic permutations #

This file develops the theory of cycles in permutations.

## Main definitions #

In the following, f : Equiv.Perm β.

The following two definitions require that β is a Fintype:

## Main results #

• This file contains several closure results:

## Notes #

Equiv.Perm.is_cycle and Equiv.Perm.IsCycleOn are different in three ways:

• is_cycle is about the entire type while IsCycleOn is restricted to a set.
• is_cycle forbids the identity while IsCycleOn allows it (if s is a subsingleton).
• IsCycleOn forbids fixed points on s (if s is nontrivial), while is_cycle allows them.

### SameCycle#

def Equiv.Perm.SameCycle {α : Type u_2} (f : ) (x : α) (y : α) :

The equivalence relation indicating that two points are in the same cycle of a permutation.

Instances For
theorem Equiv.Perm.SameCycle.refl {α : Type u_2} (f : ) (x : α) :
theorem Equiv.Perm.SameCycle.rfl {α : Type u_2} {f : } {x : α} :
theorem Eq.sameCycle {α : Type u_2} {x : α} {y : α} (h : x = y) (f : ) :
theorem Equiv.Perm.SameCycle.symm {α : Type u_2} {f : } {x : α} {y : α} :
theorem Equiv.Perm.sameCycle_comm {α : Type u_2} {f : } {x : α} {y : α} :
theorem Equiv.Perm.SameCycle.trans {α : Type u_2} {f : } {x : α} {y : α} {z : α} :
theorem Equiv.Perm.SameCycle.equivalence {α : Type u_2} (f : ) :
def Equiv.Perm.SameCycle.setoid {α : Type u_2} (f : ) :

The setoid defined by the SameCycle relation.

Instances For
@[simp]
theorem Equiv.Perm.sameCycle_one {α : Type u_2} {x : α} {y : α} :
x = y
@[simp]
theorem Equiv.Perm.sameCycle_inv {α : Type u_2} {f : } {x : α} {y : α} :
theorem Equiv.Perm.SameCycle.inv {α : Type u_2} {f : } {x : α} {y : α} :

Alias of the reverse direction of Equiv.Perm.sameCycle_inv.

theorem Equiv.Perm.SameCycle.of_inv {α : Type u_2} {f : } {x : α} {y : α} :

Alias of the forward direction of Equiv.Perm.sameCycle_inv.

@[simp]
theorem Equiv.Perm.sameCycle_conj {α : Type u_2} {f : } {g : } {x : α} {y : α} :
theorem Equiv.Perm.SameCycle.conj {α : Type u_2} {f : } {g : } {x : α} {y : α} :
Equiv.Perm.SameCycle (g * f * g⁻¹) (g x) (g y)
theorem Equiv.Perm.SameCycle.apply_eq_self_iff {α : Type u_2} {f : } {x : α} {y : α} :
→ (f x = x f y = y)
theorem Equiv.Perm.SameCycle.eq_of_left {α : Type u_2} {f : } {x : α} {y : α} (h : ) (hx : Function.IsFixedPt (f) x) :
x = y
theorem Equiv.Perm.SameCycle.eq_of_right {α : Type u_2} {f : } {x : α} {y : α} (h : ) (hy : Function.IsFixedPt (f) y) :
x = y
@[simp]
theorem Equiv.Perm.sameCycle_apply_left {α : Type u_2} {f : } {x : α} {y : α} :
@[simp]
theorem Equiv.Perm.sameCycle_apply_right {α : Type u_2} {f : } {x : α} {y : α} :
@[simp]
theorem Equiv.Perm.sameCycle_inv_apply_left {α : Type u_2} {f : } {x : α} {y : α} :
@[simp]
theorem Equiv.Perm.sameCycle_inv_apply_right {α : Type u_2} {f : } {x : α} {y : α} :
@[simp]
theorem Equiv.Perm.sameCycle_zpow_left {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f (↑(f ^ n) x) y
@[simp]
theorem Equiv.Perm.sameCycle_zpow_right {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f x (↑(f ^ n) y)
@[simp]
theorem Equiv.Perm.sameCycle_pow_left {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f (↑(f ^ n) x) y
@[simp]
theorem Equiv.Perm.sameCycle_pow_right {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f x (↑(f ^ n) y)
theorem Equiv.Perm.SameCycle.of_apply_left {α : Type u_2} {f : } {x : α} {y : α} :
Equiv.Perm.SameCycle f (f x) y

Alias of the forward direction of Equiv.Perm.sameCycle_apply_left.

theorem Equiv.Perm.SameCycle.apply_left {α : Type u_2} {f : } {x : α} {y : α} :
Equiv.Perm.SameCycle f (f x) y

Alias of the reverse direction of Equiv.Perm.sameCycle_apply_left.

theorem Equiv.Perm.SameCycle.apply_right {α : Type u_2} {f : } {x : α} {y : α} :
Equiv.Perm.SameCycle f x (f y)

Alias of the reverse direction of Equiv.Perm.sameCycle_apply_right.

theorem Equiv.Perm.SameCycle.of_apply_right {α : Type u_2} {f : } {x : α} {y : α} :
Equiv.Perm.SameCycle f x (f y)

Alias of the forward direction of Equiv.Perm.sameCycle_apply_right.

theorem Equiv.Perm.SameCycle.inv_apply_left {α : Type u_2} {f : } {x : α} {y : α} :
Equiv.Perm.SameCycle f (f⁻¹ x) y

Alias of the reverse direction of Equiv.Perm.sameCycle_inv_apply_left.

theorem Equiv.Perm.SameCycle.of_inv_apply_left {α : Type u_2} {f : } {x : α} {y : α} :
Equiv.Perm.SameCycle f (f⁻¹ x) y

Alias of the forward direction of Equiv.Perm.sameCycle_inv_apply_left.

theorem Equiv.Perm.SameCycle.inv_apply_right {α : Type u_2} {f : } {x : α} {y : α} :
Equiv.Perm.SameCycle f x (f⁻¹ y)

Alias of the reverse direction of Equiv.Perm.sameCycle_inv_apply_right.

theorem Equiv.Perm.SameCycle.of_inv_apply_right {α : Type u_2} {f : } {x : α} {y : α} :
Equiv.Perm.SameCycle f x (f⁻¹ y)

Alias of the forward direction of Equiv.Perm.sameCycle_inv_apply_right.

theorem Equiv.Perm.SameCycle.pow_left {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f (↑(f ^ n) x) y

Alias of the reverse direction of Equiv.Perm.sameCycle_pow_left.

theorem Equiv.Perm.SameCycle.of_pow_left {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f (↑(f ^ n) x) y

Alias of the forward direction of Equiv.Perm.sameCycle_pow_left.

theorem Equiv.Perm.SameCycle.of_pow_right {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f x (↑(f ^ n) y)

Alias of the forward direction of Equiv.Perm.sameCycle_pow_right.

theorem Equiv.Perm.SameCycle.pow_right {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f x (↑(f ^ n) y)

Alias of the reverse direction of Equiv.Perm.sameCycle_pow_right.

theorem Equiv.Perm.SameCycle.of_zpow_left {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f (↑(f ^ n) x) y

Alias of the forward direction of Equiv.Perm.sameCycle_zpow_left.

theorem Equiv.Perm.SameCycle.zpow_left {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f (↑(f ^ n) x) y

Alias of the reverse direction of Equiv.Perm.sameCycle_zpow_left.

theorem Equiv.Perm.SameCycle.zpow_right {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f x (↑(f ^ n) y)

Alias of the reverse direction of Equiv.Perm.sameCycle_zpow_right.

theorem Equiv.Perm.SameCycle.of_zpow_right {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle f x (↑(f ^ n) y)

Alias of the forward direction of Equiv.Perm.sameCycle_zpow_right.

theorem Equiv.Perm.SameCycle.of_pow {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle (f ^ n) x y
theorem Equiv.Perm.SameCycle.of_zpow {α : Type u_2} {f : } {x : α} {y : α} {n : } :
Equiv.Perm.SameCycle (f ^ n) x y
@[simp]
theorem Equiv.Perm.sameCycle_subtypePerm {α : Type u_2} {f : } {p : αProp} {h : ∀ (x : α), p x p (f x)} {x : { x // p x }} {y : { x // p x }} :
theorem Equiv.Perm.SameCycle.subtypePerm {α : Type u_2} {f : } {p : αProp} {h : ∀ (x : α), p x p (f x)} {x : { x // p x }} {y : { x // p x }} :
Equiv.Perm.SameCycle f x y

Alias of the reverse direction of Equiv.Perm.sameCycle_subtypePerm.

@[simp]
theorem Equiv.Perm.sameCycle_extendDomain {α : Type u_2} {β : Type u_3} {g : } {x : α} {y : α} {p : βProp} [] {f : α } :
Equiv.Perm.SameCycle () ↑(f x) ↑(f y)
theorem Equiv.Perm.SameCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : } {x : α} {y : α} {p : βProp} [] {f : α } :
Equiv.Perm.SameCycle () ↑(f x) ↑(f y)

Alias of the reverse direction of Equiv.Perm.sameCycle_extendDomain.

theorem Equiv.Perm.SameCycle.exists_pow_eq' {α : Type u_2} {f : } {x : α} {y : α} [] :
i, i < ↑(f ^ i) x = y
theorem Equiv.Perm.SameCycle.exists_pow_eq'' {α : Type u_2} {f : } {x : α} {y : α} [] (h : ) :
i x x, ↑(f ^ i) x = y
instance Equiv.Perm.instDecidableRelSameCycle {α : Type u_2} [] [] (f : ) :

### IsCycle#

def Equiv.Perm.IsCycle {α : Type u_2} (f : ) :

A cycle is a non identity permutation where any two nonfixed points of the permutation are related by repeated application of the permutation.

Instances For
theorem Equiv.Perm.IsCycle.ne_one {α : Type u_2} {f : } (h : ) :
f 1
@[simp]
theorem Equiv.Perm.not_isCycle_one {α : Type u_2} :
theorem Equiv.Perm.IsCycle.sameCycle {α : Type u_2} {f : } {x : α} {y : α} (hf : ) (hx : f x x) (hy : f y y) :
theorem Equiv.Perm.IsCycle.exists_zpow_eq {α : Type u_2} {f : } {x : α} {y : α} :
f x xf y yi, ↑(f ^ i) x = y
theorem Equiv.Perm.IsCycle.inv {α : Type u_2} {f : } (hf : ) :
@[simp]
theorem Equiv.Perm.isCycle_inv {α : Type u_2} {f : } :
theorem Equiv.Perm.IsCycle.conj {α : Type u_2} {f : } {g : } :
theorem Equiv.Perm.IsCycle.extendDomain {α : Type u_2} {β : Type u_3} {g : } {p : βProp} [] (f : α ) :
theorem Equiv.Perm.isCycle_iff_sameCycle {α : Type u_2} {f : } {x : α} (hx : f x x) :
∀ {y : α}, f y y
theorem Equiv.Perm.IsCycle.exists_pow_eq {α : Type u_2} {f : } {x : α} {y : α} [] (hf : ) (hx : f x x) (hy : f y y) :
i, ↑(f ^ i) x = y
theorem Equiv.Perm.isCycle_swap {α : Type u_2} {x : α} {y : α} [] (hxy : x y) :
theorem Equiv.Perm.IsSwap.isCycle {α : Type u_2} {f : } [] :
theorem Equiv.Perm.IsCycle.two_le_card_support {α : Type u_2} {f : } [] [] (h : ) :
theorem Equiv.Perm.IsCycle.exists_pow_eq_one {β : Type u_3} [] {f : } (hf : ) :
k x, f ^ k = 1
noncomputable def Equiv.Perm.IsCycle.zpowersEquivSupport {α : Type u_2} [] [] {σ : } (hσ : ) :
{ x // } { x // }

The subgroup generated by a cycle is in bijection with its support

Instances For
@[simp]
theorem Equiv.Perm.IsCycle.zpowersEquivSupport_apply {α : Type u_2} [] [] {σ : } (hσ : ) {n : } :
↑() { val := σ ^ n, property := (_ : y, (fun x x_1 => x ^ x_1) σ y = σ ^ n) } = { val := ↑(σ ^ n) (), property := (_ : ↑(σ ^ n) () ) }
@[simp]
theorem Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply {α : Type u_2} [] [] {σ : } (hσ : ) (n : ) :
().symm { val := ↑(σ ^ n) (), property := (_ : ↑(σ ^ n) () ) } = { val := σ ^ n, property := (_ : y, (fun x x_1 => x ^ x_1) σ y = σ ^ n) }
theorem Equiv.Perm.IsCycle.orderOf {α : Type u_2} {f : } [] [] (hf : ) :
theorem Equiv.Perm.isCycle_swap_mul_aux₁ {α : Type u_4} [] (n : ) {b : α} {x : α} {f : } :
↑(Equiv.swap x (f x) * f) b b↑(f ^ n) (f x) = bi, ↑((Equiv.swap x (f x) * f) ^ i) (f x) = b
theorem Equiv.Perm.isCycle_swap_mul_aux₂ {α : Type u_4} [] (n : ) {b : α} {x : α} {f : } :
↑(Equiv.swap x (f x) * f) b b↑(f ^ n) (f x) = bi, ↑((Equiv.swap x (f x) * f) ^ i) (f x) = b
theorem Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self {α : Type u_4} [] {f : } (hf : ) {x : α} (hfx : f x x) (hffx : f (f x) = x) :
f = Equiv.swap x (f x)
theorem Equiv.Perm.IsCycle.swap_mul {α : Type u_4} [] {f : } (hf : ) {x : α} (hx : f x x) (hffx : f (f x) x) :
theorem Equiv.Perm.IsCycle.sign {α : Type u_2} [] [] {f : } (hf : ) :
Equiv.Perm.sign f = -(-1) ^
theorem Equiv.Perm.IsCycle.of_pow {α : Type u_2} {f : } [] [] {n : } (h1 : Equiv.Perm.IsCycle (f ^ n)) (h2 : ) :
theorem Equiv.Perm.IsCycle.of_zpow {α : Type u_2} {f : } [] [] {n : } (h1 : Equiv.Perm.IsCycle (f ^ n)) (h2 : ) :
theorem Equiv.Perm.nodup_of_pairwise_disjoint_cycles {β : Type u_3} {l : List ()} (h1 : ∀ (f : ), f l) (h2 : List.Pairwise Equiv.Perm.Disjoint l) :
theorem Equiv.Perm.IsCycle.support_congr {α : Type u_2} {f : } {g : } [] [] (hf : ) (hg : ) (h : ) (h' : ∀ (x : α), f x = g x) :
f = g

Unlike support_congr, which assumes that ∀ (x ∈ g.support), f x = g x), here we have the weaker assumption that ∀ (x ∈ f.support), f x = g x.

theorem Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr {α : Type u_2} {f : } {g : } {x : α} [] [] (hf : ) (hg : ) (h : ∀ (x : α), f x = g x) (hx : f x = g x) (hx' : ) :
f = g

If two cyclic permutations agree on all terms in their intersection, and that intersection is not empty, then the two cyclic permutations must be equal.

theorem Equiv.Perm.IsCycle.support_pow_eq_iff {α : Type u_2} {f : } [] [] (hf : ) {n : } :
theorem Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf {α : Type u_2} {f : } [] [] (hf : ) {n : } (npos : 0 < n) (hn : n < ) :
theorem Equiv.Perm.IsCycle.pow_iff {β : Type u_3} [] {f : } (hf : ) {n : } :
theorem Equiv.Perm.IsCycle.pow_eq_one_iff {β : Type u_3} [] {f : } (hf : ) {n : } :
f ^ n = 1 x, f x x ↑(f ^ n) x = x
theorem Equiv.Perm.IsCycle.pow_eq_one_iff' {β : Type u_3} [] {f : } (hf : ) {n : } {x : β} (hx : f x x) :
f ^ n = 1 ↑(f ^ n) x = x
theorem Equiv.Perm.IsCycle.pow_eq_one_iff'' {β : Type u_3} [] {f : } (hf : ) {n : } :
f ^ n = 1 ∀ (x : β), f x x↑(f ^ n) x = x
theorem Equiv.Perm.IsCycle.pow_eq_pow_iff {β : Type u_3} [] {f : } (hf : ) {a : } {b : } :
f ^ a = f ^ b x, f x x ↑(f ^ a) x = ↑(f ^ b) x
theorem Equiv.Perm.IsCycle.isCycle_pow_pos_of_lt_prime_order {β : Type u_3} [] {f : } (hf : ) (hf' : Nat.Prime ()) (n : ) (hn : 0 < n) (hn' : n < ) :

### IsCycleOn#

def Equiv.Perm.IsCycleOn {α : Type u_2} (f : ) (s : Set α) :

A permutation is a cycle on s when any two points of s are related by repeated application of the permutation. Note that this means the identity is a cycle of subsingleton sets.

Instances For
@[simp]
theorem Equiv.Perm.isCycleOn_empty {α : Type u_2} {f : } :
@[simp]
theorem Equiv.Perm.isCycleOn_one {α : Type u_2} {s : Set α} :
theorem Set.Subsingleton.isCycleOn_one {α : Type u_2} {s : Set α} :

Alias of the reverse direction of Equiv.Perm.isCycleOn_one.

theorem Equiv.Perm.IsCycleOn.subsingleton {α : Type u_2} {s : Set α} :

Alias of the forward direction of Equiv.Perm.isCycleOn_one.

@[simp]
theorem Equiv.Perm.isCycleOn_singleton {α : Type u_2} {f : } {a : α} :
f a = a
theorem Equiv.Perm.isCycleOn_of_subsingleton {α : Type u_2} [] (f : ) (s : Set α) :
@[simp]
theorem Equiv.Perm.isCycleOn_inv {α : Type u_2} {f : } {s : Set α} :
theorem Equiv.Perm.IsCycleOn.inv {α : Type u_2} {f : } {s : Set α} :

Alias of the reverse direction of Equiv.Perm.isCycleOn_inv.

theorem Equiv.Perm.IsCycleOn.of_inv {α : Type u_2} {f : } {s : Set α} :

Alias of the forward direction of Equiv.Perm.isCycleOn_inv.

theorem Equiv.Perm.IsCycleOn.conj {α : Type u_2} {f : } {g : } {s : Set α} (h : ) :
Equiv.Perm.IsCycleOn (g * f * g⁻¹) (g '' s)
theorem Equiv.Perm.isCycleOn_swap {α : Type u_2} {a : α} {b : α} [] (hab : a b) :
theorem Equiv.Perm.IsCycleOn.apply_ne {α : Type u_2} {f : } {s : Set α} {a : α} (hf : ) (hs : ) (ha : a s) :
f a a
theorem Equiv.Perm.IsCycle.isCycleOn {α : Type u_2} {f : } (hf : ) :
Equiv.Perm.IsCycleOn f {x | f x x}
theorem Equiv.Perm.isCycle_iff_exists_isCycleOn {α : Type u_2} {f : } :
s, ∀ ⦃x : α⦄, ¬Function.IsFixedPt (f) xx s

This lemma demonstrates the relation between Equiv.Perm.IsCycle and Equiv.Perm.IsCycleOn in non-degenerate cases.

theorem Equiv.Perm.IsCycleOn.apply_mem_iff {α : Type u_2} {f : } {s : Set α} {x : α} (hf : ) :
f x s x s
theorem Equiv.Perm.IsCycleOn.isCycle_subtypePerm {α : Type u_2} {f : } {s : Set α} (hf : ) (hs : ) :
Equiv.Perm.IsCycle (Equiv.Perm.subtypePerm f (_ : ∀ (x : α), x s f x s))

Note that the identity satisfies IsCycleOn for any subsingleton set, but not IsCycle.

theorem Equiv.Perm.IsCycleOn.subtypePerm {α : Type u_2} {f : } {s : Set α} (hf : ) :
Equiv.Perm.IsCycleOn (Equiv.Perm.subtypePerm f (_ : ∀ (x : α), x s f x s)) Set.univ

Note that the identity is a cycle on any subsingleton set, but not a cycle.

theorem Equiv.Perm.IsCycleOn.pow_apply_eq {α : Type u_2} {f : } {a : α} {s : } (hf : ) (ha : a s) {n : } :
↑(f ^ n) a = a n
theorem Equiv.Perm.IsCycleOn.zpow_apply_eq {α : Type u_2} {f : } {a : α} {s : } (hf : ) (ha : a s) {n : } :
↑(f ^ n) a = a ↑() n
theorem Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply {α : Type u_2} {f : } {a : α} {s : } (hf : ) (ha : a s) {m : } {n : } :
↑(f ^ m) a = ↑(f ^ n) a
theorem Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply {α : Type u_2} {f : } {a : α} {s : } (hf : ) (ha : a s) {m : } {n : } :
↑(f ^ m) a = ↑(f ^ n) a m n [ZMOD ↑()]
theorem Equiv.Perm.IsCycleOn.pow_card_apply {α : Type u_2} {f : } {a : α} {s : } (hf : ) (ha : a s) :
↑(f ^ ) a = a
theorem Equiv.Perm.IsCycleOn.exists_pow_eq {α : Type u_2} {f : } {a : α} {b : α} {s : } (hf : ) (ha : a s) (hb : b s) :
n, n < ↑(f ^ n) a = b
theorem Equiv.Perm.IsCycleOn.exists_pow_eq' {α : Type u_2} {f : } {s : Set α} {a : α} {b : α} (hs : ) (hf : ) (ha : a s) (hb : b s) :
n, ↑(f ^ n) a = b
theorem Equiv.Perm.IsCycleOn.range_pow {α : Type u_2} {f : } {s : Set α} {a : α} (hs : ) (h : ) (ha : a s) :
(Set.range fun n => ↑(f ^ n) a) = s
theorem Equiv.Perm.IsCycleOn.range_zpow {α : Type u_2} {f : } {s : Set α} {a : α} (h : ) (ha : a s) :
(Set.range fun n => ↑(f ^ n) a) = s
theorem Equiv.Perm.IsCycleOn.of_pow {α : Type u_2} {f : } {s : Set α} {n : } (hf : Equiv.Perm.IsCycleOn (f ^ n) s) (h : Set.BijOn (f) s s) :
theorem Equiv.Perm.IsCycleOn.of_zpow {α : Type u_2} {f : } {s : Set α} {n : } (hf : Equiv.Perm.IsCycleOn (f ^ n) s) (h : Set.BijOn (f) s s) :
theorem Equiv.Perm.IsCycleOn.extendDomain {α : Type u_2} {β : Type u_3} {g : } {s : Set α} {p : βProp} [] (f : α ) (h : ) :
Equiv.Perm.IsCycleOn () (Subtype.val f '' s)
theorem Equiv.Perm.IsCycleOn.countable {α : Type u_2} {f : } {s : Set α} (hs : ) :

### cycleOf#

def Equiv.Perm.cycleOf {α : Type u_2} [] [] (f : ) (x : α) :

f.cycleOf x is the cycle of the permutation f to which x belongs.

Instances For
theorem Equiv.Perm.cycleOf_apply {α : Type u_2} [] [] (f : ) (x : α) (y : α) :
↑() y = if then f y else y
theorem Equiv.Perm.cycleOf_inv {α : Type u_2} [] [] (f : ) (x : α) :
@[simp]
theorem Equiv.Perm.cycleOf_pow_apply_self {α : Type u_2} [] [] (f : ) (x : α) (n : ) :
↑( ^ n) x = ↑(f ^ n) x
@[simp]
theorem Equiv.Perm.cycleOf_zpow_apply_self {α : Type u_2} [] [] (f : ) (x : α) (n : ) :
↑( ^ n) x = ↑(f ^ n) x
theorem Equiv.Perm.SameCycle.cycleOf_apply {α : Type u_2} [] [] {f : } {x : α} {y : α} :
↑() y = f y
theorem Equiv.Perm.cycleOf_apply_of_not_sameCycle {α : Type u_2} [] [] {f : } {x : α} {y : α} :
¬↑() y = y
theorem Equiv.Perm.SameCycle.cycleOf_eq {α : Type u_2} [] [] {f : } {x : α} {y : α} (h : ) :
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_zpow_self {α : Type u_2} [] [] (f : ) (x : α) (k : ) :
↑() (↑(f ^ k) x) = ↑(f ^ (k + 1)) x
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_pow_self {α : Type u_2} [] [] (f : ) (x : α) (k : ) :
↑() (↑(f ^ k) x) = ↑(f ^ (k + 1)) x
@[simp]
theorem Equiv.Perm.cycleOf_apply_apply_self {α : Type u_2} [] [] (f : ) (x : α) :
↑() (f x) = f (f x)
@[simp]
theorem Equiv.Perm.cycleOf_apply_self {α : Type u_2} [] [] (f : ) (x : α) :
↑() x = f x
theorem Equiv.Perm.IsCycle.cycleOf_eq {α : Type u_2} [] [] {f : } {x : α} (hf : ) (hx : f x x) :
= f
@[simp]
theorem Equiv.Perm.cycleOf_eq_one_iff {α : Type u_2} [] [] {x : α} (f : ) :
= 1 f x = x
@[simp]
theorem Equiv.Perm.cycleOf_self_apply {α : Type u_2} [] [] (f : ) (x : α) :
Equiv.Perm.cycleOf f (f x) =
@[simp]
theorem Equiv.Perm.cycleOf_self_apply_pow {α : Type u_2} [] [] (f : ) (n : ) (x : α) :
Equiv.Perm.cycleOf f (↑(f ^ n) x) =
@[simp]
theorem Equiv.Perm.cycleOf_self_apply_zpow {α : Type u_2} [] [] (f : ) (n : ) (x : α) :
Equiv.Perm.cycleOf f (↑(f ^ n) x) =
theorem Equiv.Perm.IsCycle.cycleOf {α : Type u_2} [] [] {f : } {x : α} (hf : ) :
= if f x = x then 1 else f
theorem Equiv.Perm.cycleOf_one {α : Type u_2} [] [] (x : α) :
= 1
theorem Equiv.Perm.isCycle_cycleOf {α : Type u_2} [] [] {x : α} (f : ) (hx : f x x) :
@[simp]
theorem Equiv.Perm.two_le_card_support_cycleOf_iff {α : Type u_2} [] [] {f : } {x : α} :
f x x
@[simp]
theorem Equiv.Perm.card_support_cycleOf_pos_iff {α : Type u_2} [] [] {f : } {x : α} :
f x x
theorem Equiv.Perm.pow_apply_eq_pow_mod_orderOf_cycleOf_apply {α : Type u_2} [] [] (f : ) (n : ) (x : α) :
↑(f ^ n) x = ↑(f ^ (n % )) x
theorem Equiv.Perm.cycleOf_mul_of_apply_right_eq_self {α : Type u_2} [] [] {f : } {g : } (h : Commute f g) (x : α) (hx : g x = x) :
theorem Equiv.Perm.Disjoint.cycleOf_mul_distrib {α : Type u_2} [] [] {f : } {g : } (h : ) (x : α) :
theorem Equiv.Perm.support_cycleOf_eq_nil_iff {α : Type u_2} [] [] {f : } {x : α} :
theorem Equiv.Perm.support_cycleOf_le {α : Type u_2} [] [] (f : ) (x : α) :
theorem Equiv.Perm.mem_support_cycleOf_iff {α : Type u_2} [] [] {f : } {x : α} {y : α} :
theorem Equiv.Perm.mem_support_cycleOf_iff' {α : Type u_2} [] [] {f : } {x : α} {y : α} (hx : f x x) :
theorem Equiv.Perm.SameCycle.mem_support_iff {α : Type u_2} [] [] {f : } {x : α} {y : α} (h : ) :
theorem Equiv.Perm.pow_mod_card_support_cycleOf_self_apply {α : Type u_2} [] [] (f : ) (n : ) (x : α) :
↑(f ^ ()) x = ↑(f ^ n) x
theorem Equiv.Perm.isCycle_cycleOf_iff {α : Type u_2} [] [] {x : α} (f : ) :
f x x

x is in the support of f iff Equiv.Perm.cycle_of f x is a cycle.

theorem Equiv.Perm.isCycleOn_support_cycleOf {α : Type u_2} [] [] (f : ) (x : α) :
theorem Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support {α : Type u_2} [] [] {f : } {x : α} {y : α} (h : ) (hx : ) :
i x, ↑(f ^ i) x = y
theorem Equiv.Perm.SameCycle.exists_pow_eq {α : Type u_2} [] [] {x : α} {y : α} (f : ) (h : ) :
i x x, ↑(f ^ i) x = y

### cycleFactors#

def Equiv.Perm.cycleFactorsAux {α : Type u_2} [] [] (l : List α) (f : ) :
(∀ {x : α}, f x xx l) → { l // = f (∀ (g : ), g l) List.Pairwise Equiv.Perm.Disjoint l }

Given a list l : List α and a permutation f : perm α whose nonfixed points are all in l, recursively factors f into cycles.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Equiv.Perm.mem_list_cycles_iff {α : Type u_4} [] {l : List ()} (h1 : ∀ (σ : ), σ l) (h2 : List.Pairwise Equiv.Perm.Disjoint l) {σ : } :
σ l ∀ (a : α), σ a aσ a = ↑() a
theorem Equiv.Perm.list_cycles_perm_list_cycles {α : Type u_4} [] {l₁ : List ()} {l₂ : List ()} (h₀ : = ) (h₁l₁ : ∀ (σ : ), σ l₁) (h₁l₂ : ∀ (σ : ), σ l₂) (h₂l₁ : List.Pairwise Equiv.Perm.Disjoint l₁) (h₂l₂ : List.Pairwise Equiv.Perm.Disjoint l₂) :
l₁ ~ l₂
def Equiv.Perm.cycleFactors {α : Type u_2} [] [] [] (f : ) :
{ l // = f (∀ (g : ), g l) List.Pairwise Equiv.Perm.Disjoint l }

Factors a permutation f into a list of disjoint cyclic permutations that multiply to f.

Instances For
def Equiv.Perm.truncCycleFactors {α : Type u_2} [] [] (f : ) :
Trunc { l // = f (∀ (g : ), g l) List.Pairwise Equiv.Perm.Disjoint l }

Factors a permutation f into a list of disjoint cyclic permutations that multiply to f, without a linear order.

Instances For
def Equiv.Perm.cycleFactorsFinset {α : Type u_2} [] [] (f : ) :

Factors a permutation f into a Finset of disjoint cyclic permutations that multiply to f.

Instances For
theorem Equiv.Perm.cycleFactorsFinset_eq_list_toFinset {α : Type u_2} [] [] {σ : } {l : List ()} (hn : ) :
(∀ (f : ), f l) List.Pairwise Equiv.Perm.Disjoint l = σ
theorem Equiv.Perm.cycleFactorsFinset_eq_finset {α : Type u_2} [] [] {σ : } {s : Finset ()} :
(∀ (f : ), f s) h, Finset.noncommProd s id (_ : Set.Pairwise s fun a b => Commute (id a) (id b)) = σ
theorem Equiv.Perm.cycleFactorsFinset_pairwise_disjoint {α : Type u_2} [] [] (f : ) :
Set.Pairwise () Equiv.Perm.Disjoint
theorem Equiv.Perm.cycleFactorsFinset_mem_commute {α : Type u_2} [] [] (f : ) :
Set.Pairwise () Commute
theorem Equiv.Perm.cycleFactorsFinset_noncommProd {α : Type u_2} [] [] (f : ) (comm : optParam (Set.Pairwise () Commute) (_ : Set.Pairwise () Commute)) :
= f

The product of cycle factors is equal to the original f : perm α.

theorem Equiv.Perm.mem_cycleFactorsFinset_iff {α : Type u_2} [] [] {f : } {p : } :
∀ (a : α), p a = f a
theorem Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff {α : Type u_2} [] [] {f : } {x : α} :
theorem Equiv.Perm.mem_cycleFactorsFinset_support_le {α : Type u_2} [] [] {p : } {f : } (h : ) :
theorem Equiv.Perm.cycleFactorsFinset_eq_empty_iff {α : Type u_2} [] [] {f : } :
@[simp]
theorem Equiv.Perm.cycleFactorsFinset_one {α : Type u_2} [] [] :
@[simp]
theorem Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton {α : Type u_2} [] [] {f : } (hf : ) :
theorem Equiv.Perm.cycleFactorsFinset_eq_singleton_iff {α : Type u_2} [] [] {f : } {g : } :
f = g
theorem Equiv.Perm.cycleFactorsFinset_injective {α : Type u_2} [] [] :
Function.Injective Equiv.Perm.cycleFactorsFinset

Two permutations f g : perm α have the same cycle factors iff they are the same.

theorem Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset {α : Type u_2} [] [] {f : } {g : } (h : ) :
theorem Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union {α : Type u_2} [] [] {f : } {g : } (h : ) :
theorem Equiv.Perm.cycle_is_cycleOf {α : Type u_2} [] [] {f : } {c : } {a : α} (ha : ) (hc : ) :
c =

If c is a cycle, a ∈ c.support and c is a cycle of f, then c = f.cycleOf a

theorem Equiv.Perm.cycle_induction_on {β : Type u_3} [] (P : ) (σ : ) (base_one : P 1) (base_cycles : (σ : ) → P σ) (induction_disjoint : (σ τ : ) → P σP τP (σ * τ)) :
P σ
theorem Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff {α : Type u_2} [] [] {f : } {g : } (h : ) :
theorem Equiv.Perm.closure_isCycle {β : Type u_3} [] :
theorem Equiv.Perm.closure_cycle_adjacent_swap {α : Type u_2} [] [] {σ : } (h1 : ) (h2 : ) (x : α) :
Subgroup.closure {σ, Equiv.swap x (σ x)} =
theorem Equiv.Perm.closure_cycle_coprime_swap {α : Type u_2} [] [] {n : } {σ : } (h0 : ) (h1 : ) (h2 : = Finset.univ) (x : α) :
Subgroup.closure {σ, Equiv.swap x (↑(σ ^ n) x)} =
theorem Equiv.Perm.closure_prime_cycle_swap {α : Type u_2} [] [] {σ : } {τ : } (h0 : ) (h1 : ) (h2 : = Finset.univ) (h3 : ) :
theorem Equiv.Perm.isConj_of_support_equiv {α : Type u_2} [] [] {σ : } {τ : } (f : { x // x ↑() } { x // x ↑() }) (hf : ∀ (x : α) (hx : x ↑()), ↑(f { val := σ x, property := (_ : σ x ) }) = τ ↑(f { val := x, property := hx })) :
IsConj σ τ
theorem Equiv.Perm.IsCycle.isConj {α : Type u_2} [] [] {σ : } {τ : } (hσ : ) (hτ : ) (h : ) :
IsConj σ τ
theorem Equiv.Perm.IsCycle.isConj_iff {α : Type u_2} [] [] {σ : } {τ : } (hσ : ) (hτ : ) :
@[simp]
theorem Equiv.Perm.support_conj {α : Type u_2} [] [] {σ : } {τ : } :
theorem Equiv.Perm.card_support_conj {α : Type u_2} [] [] {σ : } {τ : } :
theorem Equiv.Perm.Disjoint.isConj_mul {α : Type u_4} [] {σ : } {τ : } {π : } {ρ : } (hc1 : IsConj σ π) (hc2 : IsConj τ ρ) (hd1 : ) (hd2 : ) :
IsConj (σ * τ) (π * ρ)

### Fixed points #

theorem Equiv.Perm.fixed_point_card_lt_of_ne_one {α : Type u_2} [] [] {σ : } (h : σ 1) :
Finset.card (Finset.filter (fun x => σ x = x) Finset.univ) <
theorem List.Nodup.isCycleOn_formPerm {α : Type u_2} [] {l : List α} (h : ) :
theorem Finset.exists_cycleOn {α : Type u_2} [] [] (s : ) :
f,
theorem Set.Countable.exists_cycleOn {α : Type u_2} [] {s : Set α} (hs : ) :
f, {x | f x x} s
theorem Set.prod_self_eq_iUnion_perm {α : Type u_2} {f : } {s : Set α} (hf : ) :
s ×ˢ s = ⋃ (n : ), (fun a => (a, ↑(f ^ n) a)) '' s
theorem Finset.product_self_eq_disj_Union_perm_aux {α : Type u_2} {f : } {s : } (hf : ) :
Set.PairwiseDisjoint ↑() fun k => Finset.map { toFun := fun i => (i, ↑(f ^ k) i), inj' := (_ : ∀ (i j : α), (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) } s
theorem Finset.product_self_eq_disjUnion_perm {α : Type u_2} {f : } {s : } (hf : ) :
s ×ˢ s = Finset.disjiUnion () (fun k => Finset.map { toFun := fun i => (i, ↑(f ^ k) i), inj' := (_ : ∀ (i j : α), (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) } s) (_ : Set.PairwiseDisjoint ↑() fun k => Finset.map { toFun := fun i => (i, ↑(f ^ k) i), inj' := (_ : ∀ (i j : α), (fun i => (i, ↑(f ^ k) i)) i = (fun i => (i, ↑(f ^ k) i)) j((fun i => (i, ↑(f ^ k) i)) i).fst = ((fun i => (i, ↑(f ^ k) i)) j).fst) } s)

We can partition the square s ×ˢ s into shifted diagonals as such:

01234
40123
34012
23401
12340

The diagonals are given by the cycle f.

theorem Finset.sum_smul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [Module α β] {s : } {σ : } (hσ : ) (f : ια) (g : ιβ) :
((Finset.sum s fun i => f i) Finset.sum s fun i => g i) = Finset.sum () fun k => Finset.sum s fun i => f i g (↑(σ ^ k) i)
theorem Finset.sum_mul_sum_eq_sum_perm {ι : Type u_1} {α : Type u_2} [] {s : } {σ : } (hσ : ) (f : ια) (g : ια) :
((Finset.sum s fun i => f i) * Finset.sum s fun i => g i) = Finset.sum () fun k => Finset.sum s fun i => f i * g (↑(σ ^ k) i)