instIsPreprimitive — Mathlib

English

The action of the permutation group on α is preprimitive.

Русский

Действие группы перестановок на α является префримитивным.

LaTeX

$$IsPreprimitive (Perm α) α$$

Lean4

/-- The action of the permutation group of `α` on `α` is preprimitive -/
instance : IsPreprimitive (Perm α) α :=
  isPreprimitive_of_is_two_pretransitive
    (isMultiplyPretransitive _ _)
      -- This is optimal, `AlternatingGroup α` is `Nat.card α - 2`-pretransitive.

Похожие утверждения