commutator_eq_bot_or_commutator_eq_self

English

If a normal cyclic Sylow p-subgroup P has a complement K, then [K,P] is either trivial or equals P.

Русский

Если нормальная циклическая сигма-п-п-подгруппа P имеет дополнение K, то [K,P] либо тривиален, либо равен P.

LaTeX

$$$[K,P] = \\{e\\} \\quad\\lor\\quad [K,P] = P$$$

Lean4

/-- If a normal cyclic Sylow `p`-subgroup `P` has a complement `K`, then either `⁅K, P⁆ = ⊥` or
  `⁅K, P⁆ = P`. -/
theorem commutator_eq_bot_or_commutator_eq_self [P.Normal] {K : Subgroup G} (h : K.IsComplement' P) :
    ⁅K, P.1⁆ = ⊥ ∨ ⁅K, P.1⁆ = P :=
  P.2.commutator_eq_bot_or_commutator_eq_self (P.normalizer_eq_top ▸ le_top) (h.index_eq_card ▸ P.card_coprime_index)

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