isPreprimitive_of_three_le_card — Mathlib

English

Same as above: trivial blocks for alternating group action.

Русский

То же самое: тривиальные блоки для действия чередующей группы.

LaTeX

$$IsTrivialBlock B$$

Lean4

/-- The alternating group on 3 letters or more acts primitively -/
theorem isPreprimitive_of_three_le_card (h : 3 ≤ Nat.card α) : IsPreprimitive (alternatingGroup α) α :=
  letI := isPretransitive_of_three_le_card α h
  { isTrivialBlock_of_isBlock := isTrivialBlock_of_isBlock α }

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