Theorems · Theorem · group theory

SubMulAction.ofStabilizer.isMultiplyPretransitive

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [MulAction.IsPretransitive G α] {n : ℕ}
  {a : α},
  MulAction.IsMultiplyPretransitive G α n.succ ↔
    MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) n

Multiple transitivity of a pretransitive action is equivalent to one less transitivity of stabilizer of a point (Wielandt, th. 9.1, 1st part)

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

5 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsPretransitive