coe_kleinFour_of_card_eq_four — Mathlib

English

As a set inside Alt(α), KleinFour α equals {1} ∪ { g ∈ Alt(α) | (g : Perm α).cycleType = {2,2} }.

Русский

Как множество внутри Alt(α), KleinFour(α) равняется {1} ∪ { g ∈ Alt(α) | (g : Perm α).cycleType = {2,2} }.

LaTeX

$$(\mathrm{kleinFour}(\alpha) : Set(\mathrm{alternatingGroup}(\alpha))) = { 1 } \cup \{ g : \mathrm{alternatingGroup}(\alpha) \mid (g : \mathrm{Perm}(\alpha)).cycleType = \{ 2, 2 \}\}$$

Lean4

theorem coe_kleinFour_of_card_eq_four (hα4 : Nat.card α = 4) :
    (kleinFour α : Set (alternatingGroup α)) =
      { 1 } ∪ {g : alternatingGroup α | (g : Equiv.Perm α).cycleType = { 2, 2 }} :=
  by
  obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
  rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]
  exact coe_two_sylow_of_card_eq_four hα4 S

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