nontrivial_of_three_le_card — Mathlib

English

If the underlying set has at least three elements, the alternating group A_α is nontrivial.

Русский

Если в α по крайней мере три элемента, чередующаяся группа A_α не тривиальна.

LaTeX

$$$$\\operatorname{Nontrivial}(\\operatorname{alternatingGroup}(\\alpha)).$$$$

Lean4

theorem nontrivial_of_three_le_card (h3 : 3 ≤ card α) : Nontrivial (alternatingGroup α) :=
  by
  haveI := Fintype.one_lt_card_iff_nontrivial.1 (lt_trans (by decide) h3)
  rw [← Fintype.one_lt_card_iff_nontrivial]
  refine lt_of_mul_lt_mul_left ?_ (le_of_lt Nat.prime_two.pos)
  rw [two_mul_card_alternatingGroup, card_perm, ← Nat.succ_le_iff]
  exact le_trans h3 (card α).self_le_factorial

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