isNilpotent — Mathlib

English

If a finite group is the direct product of its Sylow subgroups, it is nilpotent.

Русский

Если конечная группа является прямым произведением своих подгрупп Шилова, она нильпотентна.

LaTeX

$$$\\text{IsNilpotent}(G) \\text{ if } G \\cong \\prod_p \\operatorname{Sylow}_p(G)$$$

Lean4

/-- A p-group is nilpotent -/
theorem isNilpotent [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : IsPGroup p G) : IsNilpotent G :=
  by
  cases nonempty_fintype G
  classical
  revert hG
  apply @Fintype.induction_subsingleton_or_nontrivial _ G _
  · intro _ _ _ _
    infer_instance
  · intro G _ _ ih _ h
    have hcq : Fintype.card (G ⧸ center G) < Fintype.card G :=
      by
      simp only [← Nat.card_eq_fintype_card]
      rw [card_eq_card_quotient_mul_card_subgroup (center G)]
      simp only [Nat.card_eq_fintype_card]
      apply lt_mul_of_one_lt_right
      · exact Fintype.card_pos_iff.mpr One.instNonempty
      · simp only [← Nat.card_eq_fintype_card]
        exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
    have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
    exact of_quotient_center_nilpotent hnq

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