Theorems · Definition · group theory

AddAction.IsMultiplyPreprimitive.recOn

{M : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {n : ℕ} →
          {motive : AddAction.IsMultiplyPreprimitive M α n → Sort u} →
            (t : AddAction.IsMultiplyPreprimitive M α n) →
              ((isMultiplyPretransitive : AddAction.IsMultiplyPretransitive M α n) →
                  (isPreprimitive_ofFixingAddSubgroup :
                      ∀ {s : Set α},
                        s.encard + 1 = ↑n →
                          AddAction.IsPreprimitive ↥(fixingAddSubgroup M s) ↥(SubAddAction.ofFixingAddSubgroup M s)) →
                    motive ⋯) →
                motive t

Defined in

Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddAction