# Closure results for permutation groups #

- This file contains several closure results:
`closure_isCycle`

: The symmetric group is generated by cycles`closure_cycle_adjacent_swap`

: The symmetric group is generated by a cycle and an adjacent transposition`closure_cycle_coprime_swap`

: The symmetric group is generated by a cycle and a coprime transposition`closure_prime_cycle_swap`

: The symmetric group is generated by a prime cycle and a transposition

theorem
Equiv.Perm.closure_isCycle
{β : Type u_3}
[Finite β]
:

Subgroup.closure {σ : Equiv.Perm β | σ.IsCycle} = ⊤

theorem
Equiv.Perm.closure_cycle_adjacent_swap
{α : Type u_2}
[DecidableEq α]
[Fintype α]
{σ : Equiv.Perm α}
(h1 : σ.IsCycle)
(h2 : σ.support = Finset.univ)
(x : α)
:

Subgroup.closure {σ, Equiv.swap x (σ x)} = ⊤

theorem
Equiv.Perm.closure_cycle_coprime_swap
{α : Type u_2}
[DecidableEq α]
[Fintype α]
{n : ℕ}
{σ : Equiv.Perm α}
(h0 : n.Coprime (Fintype.card α))
(h1 : σ.IsCycle)
(h2 : σ.support = Finset.univ)
(x : α)
:

Subgroup.closure {σ, Equiv.swap x ((σ ^ n) x)} = ⊤

theorem
Equiv.Perm.closure_prime_cycle_swap
{α : Type u_2}
[DecidableEq α]
[Fintype α]
{σ : Equiv.Perm α}
{τ : Equiv.Perm α}
(h0 : Nat.Prime (Fintype.card α))
(h1 : σ.IsCycle)
(h2 : σ.support = Finset.univ)
(h3 : τ.IsSwap)
:

Subgroup.closure {σ, τ} = ⊤