Theorems · Theorem · group theory

SubAddAction.ofStabilizer.isMultiplyPretransitive

∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [AddAction.IsPretransitive G α] {n : ℕ}
  {a : α},
  AddAction.IsMultiplyPretransitive G α n.succ ↔
    AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G a)) (↥(SubAddAction.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][Wielandt-1964].

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionAddAction.IsPretransitive