Theorems · Theorem · group theory

MulAction.IsPreprimitive.is_two_motive_of_is_motive

∀ {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.IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              MulAction.IsMultiplyPretransitive G α 2) ∧
            (MulAction.IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              MulAction.IsMultiplyPreprimitive G α 2)

Simultaneously prove MulAction.IsPreprimitive.is_two_pretransitive and MulAction.IsPreprimitive.is_two_preprimitive.

Defined in

Mathlib.GroupTheory.GroupAction.Jordan

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction