Theorems · Theorem · group theory

Group.isNilpotent_of_finite_tfae

∀ {G : Type u_1} [hG : Group G] [Finite G],
  [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal,
      Nonempty (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE

A finite group is nilpotent iff the normalizer condition holds, and iff all maximal groups are normal and iff all Sylow groups are normal and iff the group is the direct product of its Sylow groups.

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

2 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupFinite