commutator_alternatingGroup_eq_self

English

If n ≥ 5, the commutator of the alternating group on α equals the alternating group itself.

Русский

Если n ≥ 5, коммутатор чередующейся группы на α равен самой чередующейся группе.

LaTeX

$$$\left[ AlternatingGroup(\alpha), AlternatingGroup(\alpha) \right] = AlternatingGroup(\alpha)$$$

Lean4

/-- If `n ≥ 5`, then the alternating group on `n` letters is perfect (subgroup version) -/
theorem commutator_alternatingGroup_eq_self (h5 : 5 ≤ Fintype.card α) :
    ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α := by
  rw [← Subgroup.map_subtype_commutator, commutator_alternatingGroup_eq_top h5, ← MonoidHom.range_eq_map,
    Subgroup.range_subtype]

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