Theorems · Theorem · group theory

AddAction.ofFixingSubgroup.isMultiplyPreprimitive

∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {m n : ℕ}
  [AddAction.IsMultiplyPreprimitive M α n] {s : Set α} [Finite ↑s],
  s.ncard + m = n →
    AddAction.IsMultiplyPreprimitive (↥(fixingAddSubgroup M s)) (↥(SubAddAction.ofFixingAddSubgroup M s)) m

The fixator of a subset of cardinal d in an n-primitive action acts n-d-primitively on the remaining (d ≤ n).

Defined in

Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionAddAction.IsMultiplyPreprimitiveFinite