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_2} [Finite β] : Subgroup.closure {σ : Perm β | σ.IsCycle} = ⊤

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

theorem Equiv.Perm.closure_cycle_coprime_swap {α : Type u_1} [DecidableEq α] [Fintype α] {n : ℕ} {σ : Perm α} (h0 : n.Coprime (Fintype.card α)) (h1 : σ.IsCycle) (h2 : σ.support = Finset.univ) (x : α) : Subgroup.closure {σ, swap x ((σ ^ n) x)} = ⊤

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