Theorems · Theorem · group theory

MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_eq

∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α] (s : Set α),
  MulAction.IsMultiplyPretransitive G α s.ncard →
    (fixingSubgroup G s).index = (Nat.card α).choose s.ncard * s.ncard.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

0 results in Mathlib

Foundations

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

Assumes

GroupMulActionFinite