Theorems · Theorem · group theory

MulAction.isMultiplyPreprimitive_ofStabilizer

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

The action of stabilizer M a is one-less preprimitive.

Defined in

Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsPretransitiveMulAction.IsMultiplyPreprimitive