Theorems · Theorem · group theory

Equiv.Perm.subgroup_eq_top_of_swap_mem

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {H : Subgroup (Equiv.Perm α)}
  [d : DecidablePred fun x => x ∈ H] {τ : Equiv.Perm α},
  Nat.Prime (Fintype.card α) → Fintype.card α ∣ Fintype.card ↥H → τ ∈ H → τ.IsSwap → H = ⊤

Defined in

Mathlib.GroupTheory.Perm.Cycle.Type

Cited by

1 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqDecidablePred