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 β | Equiv.Perm.IsCycle σ} = ⊤

theorem Equiv.Perm.closure_cycle_adjacent_swap {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (h1 : Equiv.Perm.IsCycle σ) (h2 : Equiv.Perm.support σ = ⊤) (x : α) : Subgroup.closure {σ, Equiv.swap x (σ x)} = ⊤

theorem Equiv.Perm.closure_cycle_coprime_swap {α : Type u_2} [DecidableEq α] [Fintype α] {n : ℕ} {σ : Equiv.Perm α} (h0 : Nat.Coprime n (Fintype.card α)) (h1 : Equiv.Perm.IsCycle σ) (h2 : Equiv.Perm.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 : Equiv.Perm.IsCycle σ) (h2 : Equiv.Perm.support σ = Finset.univ) (h3 : Equiv.Perm.IsSwap τ) : Subgroup.closure {σ, τ} = ⊤