subsingleton_two_sylow — Mathlib

English

Let α be a finite type with four elements. Then the Sylow 2-subgroup of the alternating group on α is unique (i.e., there is only one such subgroup).

Русский

Пусть α — конечный тип сcard(α) = 4. Тогда подгруппа Sylow-2 в чередующей группе на α единственна (существует ровно одна такая подгруппа).

LaTeX

$$$\operatorname{Subsingleton}(\mathrm{Sylow}_2(\mathrm{Alt}(\alpha)))$$$

Lean4

theorem subsingleton_two_sylow (hα4 : Nat.card α = 4) : Subsingleton (Sylow 2 (alternatingGroup α)) where
  allEq S
    T := by
    rw [Sylow.ext_iff]
    simp [two_sylow_eq_kleinFour_of_card_eq_four hα4]

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