Theorems · Theorem · group theory

MulAction.isCoatom_stabilizer_iff_preprimitive

∀ (G : Type u_3) [inst : Group G] {X : Type u_4} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] [Nontrivial X]
  (a : X), IsCoatom (MulAction.stabilizer G a) ↔ MulAction.IsPreprimitive G X

A pretransitive action is preprimitive iff the stabilizer of any point is a maximal subgroup (Wielandt, th. 7.5)

Defined in

Mathlib.GroupTheory.GroupAction.Primitive

Cited by

4 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsPretransitiveNontrivial