Theorems · Theorem · group theory

Equiv.Perm.closure_cycle_coprime_swap

∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {n : ℕ} {σ : Equiv.Perm α},
  n.Coprime (Fintype.card α) →
    σ.IsCycle → σ.support = Finset.univ → ∀ (x : α), Subgroup.closure {σ, Equiv.swap x ((σ ^ n) x)} = ⊤

Defined in: Mathlib.GroupTheory.Perm.Closure
Cited by: 1 results in Mathlib
Foundations: Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites32

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
Finsetstatement and proof · cited by 13,712
Top.topstatement · cited by 9,680
Fintypestatement and proof · cited by 7,736
Subgroupstatement and proof · cited by 3,593
Finset.univstatement and proof · cited by 3,473
Finset.cardproof · cited by 2,327
Fintype.cardstatement and proof · cited by 1,386
Equiv.Permstatement and proof · cited by 1,375
le_transproof · cited by 985
eq_top_iffproof · cited by 236

Cited by1

Results whose statement or proof uses this declaration.

Equiv.Perm.closure_prime_cycle_swapproof · cited by 1