characteristic_kleinFour — Mathlib

English

For α with four elements, the Klein four subgroup of the alternating group on α is a characteristic subgroup of the alternating group.

Русский

Для α с 4 элементами Klein–четверка в чередующей группе является характеристической подгруппой самой этой группы.

LaTeX

$$$\mathrm{IsCharacteristic}(\mathrm{kleinFour}(\alpha), \mathrm{alternatingGroup}(\alpha))$$$

Lean4

theorem characteristic_kleinFour (hα4 : Nat.card α = 4) : (kleinFour α).Characteristic :=
  by
  obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
  have _ := subsingleton_two_sylow hα4
  rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]
  exact Sylow.characteristic_of_subsingleton _

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