Theorems · Theorem · group theory

MulAction.IsPreprimitive.isMultiplyPreprimitive

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsPreprimitive G α →
    ∀ {s : Set α} {n : ℕ},
      s.ncard = n + 1 →
        n + 2 < Nat.card α →
          MulAction.IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
            MulAction.IsMultiplyPreprimitive G α (n + 2)

Jordan's multiple primitivity criterion (Wielandt, 13.3)

Defined in

Mathlib.GroupTheory.GroupAction.Jordan

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction