Theorems · Theorem · group theory

MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mul

∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α] {k : ℕ},
  MulAction.IsMultiplyPretransitive G α k →
    ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k).factorial = (Nat.card α).factorial

For a multiply pretransitive action, computes the index of the fixingSubgroup of a subset of adequate cardinality

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulActionFinite