HepLean Documentation

Mathlib.GroupTheory.Perm.Closure

Closure results for permutation groups #

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 : α) :
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) :