Theorems · Theorem · group theory

IsMultiplyPretransitive.alternatingGroup_le

∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α] (G : Subgroup (Equiv.Perm α)),
  MulAction.IsMultiplyPretransitive (↥G) α (Nat.card α - 2) → alternatingGroup α ≤ G

A subgroup of Equiv.Perm α which is (card α - 2)-pretransitive contains alternatingGroup α.

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites27

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

Setproof · cited by 53,352
Fintypestatement and proof · cited by 7,736
Set.univproof · cited by 3,945
Subgroupstatement and proof · cited by 3,593
mul_commproof · cited by 2,262
LT.lt.leproof · cited by 2,189
mul_assocproof · cited by 1,667
Equiv.Permstatement and proof · cited by 1,375
Nat.cardstatement and proof · cited by 844
Nat.factorialproof · cited by 616
Set.ncardproof · cited by 344
bot_leproof · cited by 306

Cited by1

Results whose statement or proof uses this declaration.

Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_memproof · cited by 2