# mathlib3documentation

group_theory.perm.cycle.type

# Cycle Types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define the cycle type of a permutation.

## Main definitions #

• σ.cycle_type where σ is a permutation of a fintype
• σ.partition where σ is a permutation of a fintype

## Main results #

• sum_cycle_type : The sum of σ.cycle_type equals σ.support.card
• lcm_cycle_type : The lcm of σ.cycle_type equals order_of σ
• is_conj_iff_cycle_type_eq : Two permutations are conjugate if and only if they have the same cycle type.
• exists_prime_order_of_dvd_card: For every prime p dividing the order of a finite group G there exists an element of order p in G. This is known as Cauchy's theorem.
def equiv.perm.cycle_type {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :

The cycle type of a permutation

Equations
theorem equiv.perm.cycle_type_def {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
theorem equiv.perm.cycle_type_eq' {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (s : finset (equiv.perm α)) (h1 : (f : , f s f.is_cycle) (h2 : s.pairwise equiv.perm.disjoint) (h0 : _ = σ) :
theorem equiv.perm.cycle_type_eq {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (l : list (equiv.perm α)) (h0 : l.prod = σ) (h1 : (σ : , σ l σ.is_cycle) (h2 : l) :
theorem equiv.perm.cycle_type_one {α : Type u_1} [fintype α] [decidable_eq α] :
theorem equiv.perm.cycle_type_eq_zero {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
σ.cycle_type = 0 σ = 1
theorem equiv.perm.card_cycle_type_eq_zero {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
σ = 1
theorem equiv.perm.two_le_of_mem_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} {n : } (h : n σ.cycle_type) :
2 n
theorem equiv.perm.one_lt_of_mem_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} {n : } (h : n σ.cycle_type) :
1 < n
theorem equiv.perm.is_cycle.cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (hσ : σ.is_cycle) :
theorem equiv.perm.card_cycle_type_eq_one {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
theorem equiv.perm.disjoint.cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} (h : σ.disjoint τ) :
* τ).cycle_type =
theorem equiv.perm.cycle_type_inv {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
theorem equiv.perm.cycle_type_conj {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} :
theorem equiv.perm.sum_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
theorem equiv.perm.sign_of_cycle_type' {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
= (multiset.map (λ (n : ), -(-1) ^ n) σ.cycle_type).prod
theorem equiv.perm.sign_of_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] (f : equiv.perm α) :
= (-1) ^
theorem equiv.perm.lcm_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
theorem equiv.perm.dvd_of_mem_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} {n : } (h : n σ.cycle_type) :
n
theorem equiv.perm.order_of_cycle_of_dvd_order_of {α : Type u_1} [fintype α] [decidable_eq α] (f : equiv.perm α) (x : α) :
theorem equiv.perm.two_dvd_card_support {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (hσ : σ ^ 2 = 1) :
theorem equiv.perm.cycle_type_prime_order {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (hσ : nat.prime (order_of σ)) :
theorem equiv.perm.is_cycle_of_prime_order {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (h1 : nat.prime (order_of σ)) (h2 : σ.support.card < 2 * ) :
theorem equiv.perm.is_conj_of_cycle_type_eq {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} (h : σ.cycle_type = τ.cycle_type) :
τ
theorem equiv.perm.is_conj_iff_cycle_type_eq {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} :
τ
@[simp]
theorem equiv.perm.cycle_type_extend_domain {α : Type u_1} [fintype α] [decidable_eq α] {β : Type u_2} [fintype β] [decidable_eq β] {p : β Prop} (f : α ) {g : equiv.perm α} :
theorem equiv.perm.cycle_type_of_subtype {α : Type u_1} [fintype α] [decidable_eq α] {p : α Prop} {g : equiv.perm (subtype p)} :
theorem equiv.perm.mem_cycle_type_iff {α : Type u_1} [fintype α] [decidable_eq α] {n : } {σ : equiv.perm α} :
n σ.cycle_type (c τ : , σ = c * τ c.disjoint τ c.is_cycle c.support.card = n
theorem equiv.perm.le_card_support_of_mem_cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {n : } {σ : equiv.perm α} (h : n σ.cycle_type) :
theorem equiv.perm.cycle_type_of_card_le_mem_cycle_type_add_two {α : Type u_1} [fintype α] [decidable_eq α] {n : } {g : equiv.perm α} (hn2 : < n + 2) (hng : n g.cycle_type) :
theorem equiv.perm.card_compl_support_modeq {α : Type u_1} [fintype α] [decidable_eq α] {p n : } [hp : fact (nat.prime p)] {σ : equiv.perm α} (hσ : σ ^ p ^ n = 1) :
theorem equiv.perm.exists_fixed_point_of_prime {α : Type u_1} [fintype α] {p n : } [hp : fact (nat.prime p)] (hα : ¬) {σ : equiv.perm α} (hσ : σ ^ p ^ n = 1) :
(a : α), σ a = a
theorem equiv.perm.exists_fixed_point_of_prime' {α : Type u_1} [fintype α] {p n : } [hp : fact (nat.prime p)] (hα : p ) {σ : equiv.perm α} (hσ : σ ^ p ^ n = 1) {a : α} (ha : σ a = a) :
(b : α), σ b = b b a
theorem equiv.perm.is_cycle_of_prime_order' {α : Type u_1} [fintype α] {σ : equiv.perm α} (h1 : nat.prime (order_of σ)) (h2 : < 2 * ) :
theorem equiv.perm.is_cycle_of_prime_order'' {α : Type u_1} [fintype α] {σ : equiv.perm α} (h1 : nat.prime (fintype.card α)) (h2 : = ) :
def equiv.perm.vectors_prod_eq_one (G : Type u_2) [group G] (n : ) :
set (vector G n)

The type of vectors with terms from G, length n, and product equal to 1:G.

Equations
Instances for ↥equiv.perm.vectors_prod_eq_one
theorem equiv.perm.vectors_prod_eq_one.mem_iff (G : Type u_2) [group G] {n : } (v : n) :
@[protected, instance]
Equations
@[protected, instance]
Equations
def equiv.perm.vectors_prod_eq_one.vector_equiv (G : Type u_2) [group G] (n : ) :
n (n + 1))

Given a vector v of length n, make a vector of length n + 1 whose product is 1, by appending the inverse of the product of v.

Equations
@[simp]
theorem equiv.perm.vectors_prod_eq_one.vector_equiv_symm_apply (G : Type u_2) [group G] (n : ) (v : (n + 1))) :
@[simp]
def equiv.perm.vectors_prod_eq_one.equiv_vector (G : Type u_2) [group G] (n : ) :
(n - 1)

Given a vector v of length n whose product is 1, make a vector of length n - 1, by deleting the last entry of v.

Equations
@[protected, instance]
Equations
theorem equiv.perm.vectors_prod_eq_one.card (G : Type u_2) [group G] (n : ) [fintype G] :
= ^ (n - 1)
def equiv.perm.vectors_prod_eq_one.rotate {G : Type u_2} [group G] {n : } (v : ) (k : ) :

Rotate a vector whose product is 1.

Equations
theorem equiv.perm.vectors_prod_eq_one.rotate_zero {G : Type u_2} [group G] {n : } (v : ) :
theorem equiv.perm.vectors_prod_eq_one.rotate_rotate {G : Type u_2} [group G] {n : } (v : ) (j k : ) :
theorem equiv.perm.vectors_prod_eq_one.rotate_length {G : Type u_2} [group G] {n : } (v : ) :
theorem exists_prime_order_of_dvd_card {G : Type u_1} [group G] [fintype G] (p : ) [hp : fact (nat.prime p)] (hdvd : p ) :
(x : G), = p

For every prime p dividing the order of a finite group G there exists an element of order p in G. This is known as Cauchy's theorem.

theorem exists_prime_add_order_of_dvd_card {G : Type u_1} [add_group G] [fintype G] (p : ) [hp : fact (nat.prime p)] (hdvd : p ) :
(x : G),

For every prime p dividing the order of a finite additive group G there exists an element of order p in G. This is the additive version of Cauchy's theorem.

theorem equiv.perm.subgroup_eq_top_of_swap_mem {α : Type u_1} [fintype α] [decidable_eq α] {H : subgroup (equiv.perm α)} [d : decidable_pred (λ (_x : equiv.perm α), _x H)] {τ : equiv.perm α} (h0 : nat.prime (fintype.card α)) (h1 : ) (h2 : τ H) (h3 : τ.is_swap) :
H =
def equiv.perm.partition {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :

The partition corresponding to a permutation

Equations
theorem equiv.perm.parts_partition {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
theorem equiv.perm.partition_eq_of_is_conj {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} :
τ

### 3-cycles #

def equiv.perm.is_three_cycle {α : Type u_1} [fintype α] [decidable_eq α] (σ : equiv.perm α) :
Prop

A three-cycle is a cycle of length 3.

Equations
theorem equiv.perm.is_three_cycle.cycle_type {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (h : σ.is_three_cycle) :
σ.cycle_type = {3}
theorem card_support_eq_three_iff {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} :
theorem equiv.perm.is_three_cycle.sign {α : Type u_1} [fintype α] [decidable_eq α] {σ : equiv.perm α} (h : σ.is_three_cycle) :
theorem equiv.perm.is_three_cycle.inv {α : Type u_1} [fintype α] [decidable_eq α] {f : equiv.perm α} (h : f.is_three_cycle) :
@[simp]
theorem equiv.perm.is_three_cycle.inv_iff {α : Type u_1} [fintype α] [decidable_eq α] {f : equiv.perm α} :
theorem equiv.perm.is_three_cycle.order_of {α : Type u_1} [fintype α] [decidable_eq α] {g : equiv.perm α} (ht : g.is_three_cycle) :
= 3
theorem equiv.perm.is_three_cycle_swap_mul_swap_same {α : Type u_1} [fintype α] [decidable_eq α] {a b c : α} (ab : a b) (ac : a c) (bc : b c) :
theorem equiv.perm.swap_mul_swap_same_mem_closure_three_cycles {α : Type u_1} [fintype α] [decidable_eq α] {a b c : α} (ab : a b) (ac : a c) :
theorem equiv.perm.is_swap.mul_mem_closure_three_cycles {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : equiv.perm α} (hσ : σ.is_swap) (hτ : τ.is_swap) :