Theorems · Theorem · group theory

isNilpotent_of_finite_tfae

Deprecated since 2026-03-25Use Group.isNilpotent_of_finite_tfae instead.

∀ {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

Alias of Group.isNilpotent_of_finite_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

0 results in Mathlib

Foundations

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

Assumes

GroupFinite