Theorems · Theorem · group theory

normalClosure_of_stabilizer_eq_top

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  2 < ENat.card α →
    MulAction.IsMultiplyPretransitive G α 2 → ∀ {a : α}, Subgroup.normalClosure ↑(MulAction.stabilizer G a) = ⊤

In a 2-transitive action, the normal closure of stabilizers is the full group.

Defined in

Mathlib.GroupTheory.GroupAction.Jordan

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulAction