isPretransitive_of_three_le_card — Mathlib

English

If 3 ≤ |α|, then alternatingGroup α is pretransitive on α.

Русский

Если |α| ≥ 3, то для α чередующаяся группа является предтранситивной на α.

LaTeX

$$isPretransitive (alternatingGroup α) α$$

Lean4

/-- The alternating group on 3 letters or more acts transitively. -/
theorem isPretransitive_of_three_le_card (h : 3 ≤ Nat.card α) : IsPretransitive (alternatingGroup α) α :=
  by
  rw [← is_one_pretransitive_iff]
  letI := isMultiplyPretransitive α
  apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)
  rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_trans (by norm_num) h)]

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