Theorems · Theorem · group theory

SubMulAction.ofFixingSubgroup.isMultiplyPretransitive

∀ (G : Type u_1) {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {m n : ℕ}
  [Hn : MulAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s],
  s.ncard + m = n → MulAction.IsMultiplyPretransitive (↥(fixingSubgroup G s)) (↥(SubMulAction.ofFixingSubgroup G s)) m

The fixingSubgroup of a finite subset of cardinal d in an n-transitive action acts n-d-transitively on the complement.

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

4 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsMultiplyPretransitiveFinite