normal_kleinFour — Mathlib

English

For |α| = 4, Klein four is a normal subgroup of the alternating group on α.

Русский

При |α| = 4 Klein–четверка является нормальной подгруппой чередующей группы над α.

LaTeX

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

Lean4

theorem normal_kleinFour (hα4 : Nat.card α = 4) : (kleinFour α).Normal :=
  by
  have _ := characteristic_kleinFour hα4
  apply Subgroup.normal_of_characteristic

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