Theorems · Theorem · group theory

surjective_of_isSwap_of_isPretransitive

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α] [Finite α]
  (S : Set G),
  (∀ σ ∈ S, ((MulAction.toPermHom G α) σ).IsSwap) →
    Subgroup.closure S = ⊤ → ∀ [h : MulAction.IsPretransitive G α], Function.Surjective ⇑(MulAction.toPermHom G α)

A transitive permutation group generated by transpositions must be the whole symmetric group

Defined in

Mathlib.GroupTheory.Perm.ClosureSwap

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulActionDecidableEqFiniteMulAction.IsPretransitive