Nilpotent groups

An API for nilpotent groups, that is, groups for which the upper central series reaches ⊤.

Main definitions

Recall that if H K : Subgroup G then ⁅H, K⁆ : Subgroup G is the subgroup of G generated by the commutators hkh⁻¹k⁻¹. Recall also Lean's conventions that ⊤ denotes the subgroup G of G, and ⊥ denotes the trivial subgroup {1}.

• upperCentralSeries G : ℕ → Subgroup G : the upper central series of a group G. This is an increasing sequence of normal subgroups H n of G with H 0 = ⊥ and H (n + 1) / H n is the centre of G / H n.
• lowerCentralSeries G : ℕ → Subgroup G : the lower central series of a group G. This is a decreasing sequence of normal subgroups H n of G with H 0 = ⊤ and H (n + 1) = ⁅H n, G⁆.
• IsNilpotent : A group G is nilpotent if its upper central series reaches ⊤, or equivalently if its lower central series reaches ⊥.
• nilpotency_class : the length of the upper central series of a nilpotent group.
• IsAscendingCentralSeries (H : ℕ → Subgroup G) : Prop and
• IsDescendingCentralSeries (H : ℕ → Subgroup G) : Prop : Note that in the literature a "central series" for a group is usually defined to be a finite sequence of normal subgroups H 0, H 1, ..., starting at ⊤, finishing at ⊥, and with each H n / H (n + 1) central in G / H (n + 1). In this formalisation it is convenient to have two weaker predicates on an infinite sequence of subgroups H n of G: we say a sequence is a descending central series if it starts at G and ⁅H n, ⊤⁆ ⊆ H (n + 1) for all n. Note that this series may not terminate at ⊥, and the H i need not be normal. Similarly a sequence is an ascending central series if H 0 = ⊥ and ⁅H (n + 1), ⊤⁆ ⊆ H n for all n, again with no requirement that the series reaches ⊤ or that the H i are normal.

Main theorems

G is defined to be nilpotent if the upper central series reaches ⊤.

• nilpotent_iff_finite_ascending_central_series : G is nilpotent iff some ascending central series reaches ⊤.
• nilpotent_iff_finite_descending_central_series : G is nilpotent iff some descending central series reaches ⊥.
• nilpotent_iff_lower : G is nilpotent iff the lower central series reaches ⊥.
• The nilpotency_class can likewise be obtained from these equivalent definitions, see least_ascending_central_series_length_eq_nilpotencyClass, least_descending_central_series_length_eq_nilpotencyClass and lowerCentralSeries_length_eq_nilpotencyClass.
• If G is nilpotent, then so are its subgroups, images, quotients and preimages. Binary and finite products of nilpotent groups are nilpotent. Infinite products are nilpotent if their nilpotent class is bounded. Corresponding lemmas about the nilpotency_class are provided.
• The nilpotency_class of G ⧸ center G is given explicitly, and an induction principle is derived from that.
• IsNilpotent.to_isSolvable: If G is nilpotent, it is solvable.

Warning

A "central series" is usually defined to be a finite sequence of normal subgroups going from ⊥ to ⊤ with the property that each subquotient is contained within the centre of the associated quotient of G. This means that if G is not nilpotent, then none of what we have called upperCentralSeries G, lowerCentralSeries G or the sequences satisfying IsAscendingCentralSeries or IsDescendingCentralSeries are actually central series. Note that the fact that the upper and lower central series are not central series if G is not nilpotent is a standard abuse of notation.

def upperCentralSeriesStep {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : Subgroup G

If H is a normal subgroup of G, then the set {x : G | ∀ y : G, x*y*x⁻¹*y⁻¹ ∈ H} is a subgroup of G (because it is the preimage in G of the centre of the quotient group G/H.)

Equations

• upperCentralSeriesStep H = { carrier := {x : G | ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem mem_upperCentralSeriesStep {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] (x : G) : x ∈ upperCentralSeriesStep H ↔ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H

theorem upperCentralSeriesStep_eq_comap_center {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : upperCentralSeriesStep H = Subgroup.comap (QuotientGroup.mk' H) (Subgroup.center (G ⧸ H))

The proof that upperCentralSeriesStep H is the preimage of the centre of G/H under the canonical surjection.

instance instNormalUpperCentralSeriesStep {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : (upperCentralSeriesStep H).Normal

Equations

• ⋯ = ⋯

def upperCentralSeriesAux (G : Type u_1) [Group G] : ℕ → (H : Subgroup G) ×' H.Normal

An auxiliary type-theoretic definition defining both the upper central series of a group, and a proof that it is normal, all in one go.

Equations

• upperCentralSeriesAux G 0 = ⟨⊥, ⋯⟩
• upperCentralSeriesAux G n.succ = let un := upperCentralSeriesAux G n; let _un_normal := ⋯; ⟨upperCentralSeriesStep un.fst, ⋯⟩

def upperCentralSeries (G : Type u_1) [Group G] (n : ℕ) : Subgroup G

upperCentralSeries G n is the nth term in the upper central series of G.

Equations

• upperCentralSeries G n = (upperCentralSeriesAux G n).fst

instance upperCentralSeries_normal (G : Type u_1) [Group G] (n : ℕ) : (upperCentralSeries G n).Normal

Equations

• ⋯ = ⋯

@[simp]

theorem upperCentralSeries_zero (G : Type u_1) [Group G] : upperCentralSeries G 0 = ⊥

@[simp]

theorem upperCentralSeries_one (G : Type u_1) [Group G] : upperCentralSeries G 1 = Subgroup.center G

theorem mem_upperCentralSeries_succ_iff (G : Type u_1) [Group G] (n : ℕ) (x : G) : x ∈ upperCentralSeries G (n + 1) ↔ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n

The n+1st term of the upper central series H i has underlying set equal to the x such that ⁅x,G⁆ ⊆ H n

class Group.IsNilpotent (G : Type u_2) [Group G] : Prop

A group G is nilpotent if its upper central series is eventually G.

• nilpotent' : ∃ (n : ℕ), upperCentralSeries G n = ⊤

theorem Group.IsNilpotent.nilpotent' {G : Type u_2} [Group G] [self : Group.IsNilpotent G] : ∃ (n : ℕ), upperCentralSeries G n = ⊤

theorem Group.IsNilpotent.nilpotent (G : Type u_2) [Group G] [Group.IsNilpotent G] : ∃ (n : ℕ), upperCentralSeries G n = ⊤

def IsAscendingCentralSeries {G : Type u_1} [Group G] (H : ℕ → Subgroup G) : Prop

A sequence of subgroups of G is an ascending central series if H 0 is trivial and ⁅H (n + 1), G⁆ ⊆ H n for all n. Note that we do not require that H n = G for some n.

Equations

• IsAscendingCentralSeries H = (H 0 = ⊥ ∧ ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n)

def IsDescendingCentralSeries {G : Type u_1} [Group G] (H : ℕ → Subgroup G) : Prop

A sequence of subgroups of G is a descending central series if H 0 is G and ⁅H n, G⁆ ⊆ H (n + 1) for all n. Note that we do not require that H n = {1} for some n.

Equations

• IsDescendingCentralSeries H = (H 0 = ⊤ ∧ ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1))

theorem ascending_central_series_le_upper {G : Type u_1} [Group G] (H : ℕ → Subgroup G) (hH : IsAscendingCentralSeries H) (n : ℕ) : H n ≤ upperCentralSeries G n

Any ascending central series for a group is bounded above by the upper central series.

theorem upperCentralSeries_isAscendingCentralSeries (G : Type u_1) [Group G] : IsAscendingCentralSeries (upperCentralSeries G)

The upper central series of a group is an ascending central series.

theorem upperCentralSeries_mono (G : Type u_1) [Group G] : Monotone (upperCentralSeries G)

theorem nilpotent_iff_finite_ascending_central_series (G : Type u_1) [Group G] : Group.IsNilpotent G ↔ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤

A group G is nilpotent iff there exists an ascending central series which reaches G in finitely many steps.

theorem is_decending_rev_series_of_is_ascending (G : Type u_1) [Group G] {H : ℕ → Subgroup G} {n : ℕ} (hn : H n = ⊤) (hasc : IsAscendingCentralSeries H) : IsDescendingCentralSeries fun (m : ℕ) => H (n - m)

theorem is_ascending_rev_series_of_is_descending (G : Type u_1) [Group G] {H : ℕ → Subgroup G} {n : ℕ} (hn : H n = ⊥) (hdesc : IsDescendingCentralSeries H) : IsAscendingCentralSeries fun (m : ℕ) => H (n - m)

theorem nilpotent_iff_finite_descending_central_series (G : Type u_1) [Group G] : Group.IsNilpotent G ↔ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsDescendingCentralSeries H ∧ H n = ⊥

A group G is nilpotent iff there exists a descending central series which reaches the trivial group in a finite time.

def lowerCentralSeries (G : Type u_2) [Group G] : ℕ → Subgroup G

The lower central series of a group G is a sequence H n of subgroups of G, defined by H 0 is all of G and for n≥1, H (n + 1) = ⁅H n, G⁆

Equations

• lowerCentralSeries G 0 = ⊤
• lowerCentralSeries G n.succ = ⁅lowerCentralSeries G n, ⊤⁆

@[simp]

theorem lowerCentralSeries_zero {G : Type u_1} [Group G] : lowerCentralSeries G 0 = ⊤

@[simp]

theorem lowerCentralSeries_one {G : Type u_1} [Group G] : lowerCentralSeries G 1 = commutator G

theorem mem_lowerCentralSeries_succ_iff {G : Type u_1} [Group G] (n : ℕ) (q : G) : q ∈ lowerCentralSeries G (n + 1) ↔ q ∈ Subgroup.closure {x : G | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}

theorem lowerCentralSeries_succ {G : Type u_1} [Group G] (n : ℕ) : lowerCentralSeries G (n + 1) = Subgroup.closure {x : G | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}

instance lowerCentralSeries_normal {G : Type u_1} [Group G] (n : ℕ) : (lowerCentralSeries G n).Normal

Equations

• ⋯ = ⋯

theorem lowerCentralSeries_antitone {G : Type u_1} [Group G] : Antitone (lowerCentralSeries G)

theorem lowerCentralSeries_isDescendingCentralSeries {G : Type u_1} [Group G] : IsDescendingCentralSeries (lowerCentralSeries G)

The lower central series of a group is a descending central series.

theorem descending_central_series_ge_lower {G : Type u_1} [Group G] (H : ℕ → Subgroup G) (hH : IsDescendingCentralSeries H) (n : ℕ) : lowerCentralSeries G n ≤ H n

Any descending central series for a group is bounded below by the lower central series.

theorem nilpotent_iff_lowerCentralSeries {G : Type u_1} [Group G] : Group.IsNilpotent G ↔ ∃ (n : ℕ), lowerCentralSeries G n = ⊥

A group is nilpotent if and only if its lower central series eventually reaches the trivial subgroup.

noncomputable def Group.nilpotencyClass (G : Type u_1) [Group G] [hG : Group.IsNilpotent G] : ℕ

The nilpotency class of a nilpotent group is the smallest natural n such that the n'th term of the upper central series is G.

Equations

• Group.nilpotencyClass G = Nat.find ⋯

@[simp]

theorem upperCentralSeries_nilpotencyClass {G : Type u_1} [Group G] [hG : Group.IsNilpotent G] : upperCentralSeries G (Group.nilpotencyClass G) = ⊤

theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le {G : Type u_1} [Group G] [hG : Group.IsNilpotent G] {n : ℕ} : upperCentralSeries G n = ⊤ ↔ Group.nilpotencyClass G ≤ n

theorem least_ascending_central_series_length_eq_nilpotencyClass {G : Type u_1} [Group G] [hG : Group.IsNilpotent G] : Nat.find ⋯ = Group.nilpotencyClass G

The nilpotency class of a nilpotent G is equal to the smallest n for which an ascending central series reaches G in its n'th term.

theorem least_descending_central_series_length_eq_nilpotencyClass {G : Type u_1} [Group G] [hG : Group.IsNilpotent G] : Nat.find ⋯ = Group.nilpotencyClass G

The nilpotency class of a nilpotent G is equal to the smallest n for which the descending central series reaches ⊥ in its n'th term.

theorem lowerCentralSeries_length_eq_nilpotencyClass {G : Type u_1} [Group G] [hG : Group.IsNilpotent G] : Nat.find ⋯ = Group.nilpotencyClass G

The nilpotency class of a nilpotent G is equal to the length of the lower central series.

@[simp]

theorem lowerCentralSeries_nilpotencyClass {G : Type u_1} [Group G] [hG : Group.IsNilpotent G] : lowerCentralSeries G (Group.nilpotencyClass G) = ⊥

theorem lowerCentralSeries_eq_bot_iff_nilpotencyClass_le {G : Type u_1} [Group G] [hG : Group.IsNilpotent G] {n : ℕ} : lowerCentralSeries G n = ⊥ ↔ Group.nilpotencyClass G ≤ n

theorem lowerCentralSeries_map_subtype_le {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : Subgroup.map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n

instance Subgroup.isNilpotent {G : Type u_1} [Group G] (H : Subgroup G) [hG : Group.IsNilpotent G] : Group.IsNilpotent ↥H

A subgroup of a nilpotent group is nilpotent

Equations

• ⋯ = ⋯

theorem Subgroup.nilpotencyClass_le {G : Type u_1} [Group G] (H : Subgroup G) [hG : Group.IsNilpotent G] : Group.nilpotencyClass ↥H ≤ Group.nilpotencyClass G

The nilpotency class of a subgroup is less or equal to the nilpotency class of the group

@[instance 100]

instance Group.isNilpotent_of_subsingleton {G : Type u_1} [Group G] [Subsingleton G] : Group.IsNilpotent G

Equations

• ⋯ = ⋯

theorem upperCentralSeries.map {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : G →* H} (h : Function.Surjective ⇑f) (n : ℕ) : Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n

theorem lowerCentralSeries.map {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (n : ℕ) : Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n

theorem lowerCentralSeries_succ_eq_bot {G : Type u_1} [Group G] {n : ℕ} (h : lowerCentralSeries G n ≤ Subgroup.center G) : lowerCentralSeries G (n + 1) = ⊥

theorem isNilpotent_of_ker_le_center {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (hf1 : f.ker ≤ Subgroup.center G) (hH : Group.IsNilpotent H) : Group.IsNilpotent G

The preimage of a nilpotent group is nilpotent if the kernel of the homomorphism is contained in the center

theorem nilpotencyClass_le_of_ker_le_center {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (hf1 : f.ker ≤ Subgroup.center G) (hH : Group.IsNilpotent H) : Group.nilpotencyClass G ≤ Group.nilpotencyClass H + 1

theorem nilpotent_of_surjective {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] [h : Group.IsNilpotent G] (f : G →* G') (hf : Function.Surjective ⇑f) : Group.IsNilpotent G'

The range of a surjective homomorphism from a nilpotent group is nilpotent

theorem nilpotencyClass_le_of_surjective {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] (f : G →* G') (hf : Function.Surjective ⇑f) [h : Group.IsNilpotent G] : Group.nilpotencyClass G' ≤ Group.nilpotencyClass G

The nilpotency class of the range of a surjective homomorphism from a nilpotent group is less or equal the nilpotency class of the domain

theorem nilpotent_of_mulEquiv {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] [_h : Group.IsNilpotent G] (f : G ≃* G') : Group.IsNilpotent G'

Nilpotency respects isomorphisms

instance nilpotent_quotient_of_nilpotent {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [_h : Group.IsNilpotent G] : Group.IsNilpotent (G ⧸ H)

A quotient of a nilpotent group is nilpotent

Equations

• ⋯ = ⋯

theorem nilpotencyClass_quotient_le {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [_h : Group.IsNilpotent G] : Group.nilpotencyClass (G ⧸ H) ≤ Group.nilpotencyClass G

The nilpotency class of a quotient of G is less or equal the nilpotency class of G

theorem comap_upperCentralSeries_quotient_center {G : Type u_1} [Group G] (n : ℕ) : Subgroup.comap (QuotientGroup.mk' (Subgroup.center G)) (upperCentralSeries (G ⧸ Subgroup.center G) n) = upperCentralSeries G n.succ

theorem nilpotencyClass_zero_iff_subsingleton {G : Type u_1} [Group G] [Group.IsNilpotent G] : Group.nilpotencyClass G = 0 ↔ Subsingleton G

theorem nilpotencyClass_quotient_center {G : Type u_1} [Group G] [hH : Group.IsNilpotent G] : Group.nilpotencyClass (G ⧸ Subgroup.center G) = Group.nilpotencyClass G - 1

Quotienting the center G reduces the nilpotency class by 1

theorem nilpotencyClass_eq_quotient_center_plus_one {G : Type u_1} [Group G] [hH : Group.IsNilpotent G] [Nontrivial G] : Group.nilpotencyClass G = Group.nilpotencyClass (G ⧸ Subgroup.center G) + 1

The nilpotency class of a non-trivial group is one more than its quotient by the center

theorem of_quotient_center_nilpotent {G : Type u_1} [Group G] (h : Group.IsNilpotent (G ⧸ Subgroup.center G)) : Group.IsNilpotent G

If the quotient by center G is nilpotent, then so is G.

theorem nilpotent_center_quotient_ind {P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop} (G : Type u_2) [Group G] [Group.IsNilpotent G] (hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G) (hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ Subgroup.center G) → P G) : P G

A custom induction principle for nilpotent groups. The base case is a trivial group (subsingleton G), and in the induction step, one can assume the hypothesis for the group quotiented by its center.

theorem derived_le_lower_central {G : Type u_1} [Group G] (n : ℕ) : derivedSeries G n ≤ lowerCentralSeries G n

@[instance 100]

instance CommGroup.isNilpotent {G : Type u_2} [CommGroup G] : Group.IsNilpotent G

Abelian groups are nilpotent

Equations

• ⋯ = ⋯

theorem CommGroup.nilpotencyClass_le_one {G : Type u_2} [CommGroup G] : Group.nilpotencyClass G ≤ 1

Abelian groups have nilpotency class at most one

def commGroupOfNilpotencyClass {G : Type u_1} [Group G] [Group.IsNilpotent G] (h : Group.nilpotencyClass G ≤ 1) : CommGroup G

Groups with nilpotency class at most one are abelian

Equations

• commGroupOfNilpotencyClass h = Group.commGroupOfCenterEqTop ⋯

theorem lowerCentralSeries_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] (n : ℕ) : lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)

instance isNilpotent_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [Group.IsNilpotent G₁] [Group.IsNilpotent G₂] : Group.IsNilpotent (G₁ × G₂)

Products of nilpotent groups are nilpotent

Equations

• ⋯ = ⋯

theorem nilpotencyClass_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [Group.IsNilpotent G₁] [Group.IsNilpotent G₂] : Group.nilpotencyClass (G₁ × G₂) = max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂)

The nilpotency class of a product is the max of the nilpotency classes of the factors

theorem lowerCentralSeries_pi_le {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] (n : ℕ) : lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun (i : η) => lowerCentralSeries (Gs i) n

theorem isNilpotent_pi_of_bounded_class {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] [∀ (i : η), Group.IsNilpotent (Gs i)] (n : ℕ) (h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n) : Group.IsNilpotent ((i : η) → Gs i)

products of nilpotent groups are nilpotent if their nilpotency class is bounded

theorem lowerCentralSeries_pi_of_finite {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] [Finite η] (n : ℕ) : lowerCentralSeries ((i : η) → Gs i) n = Subgroup.pi Set.univ fun (i : η) => lowerCentralSeries (Gs i) n

instance isNilpotent_pi {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] [Finite η] [∀ (i : η), Group.IsNilpotent (Gs i)] : Group.IsNilpotent ((i : η) → Gs i)

n-ary products of nilpotent groups are nilpotent

Equations

• ⋯ = ⋯

theorem nilpotencyClass_pi {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] [Fintype η] [∀ (i : η), Group.IsNilpotent (Gs i)] : Group.nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun (i : η) => Group.nilpotencyClass (Gs i)

The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors

@[instance 100]

instance IsNilpotent.to_isSolvable {G : Type u_1} [Group G] [h : Group.IsNilpotent G] : IsSolvable G

A nilpotent subgroup is solvable

Equations

• ⋯ = ⋯

theorem normalizerCondition_of_isNilpotent {G : Type u_1} [Group G] [h : Group.IsNilpotent G] : NormalizerCondition G

theorem IsPGroup.isNilpotent {G : Type u_1} [hG : Group G] [Finite G] {p : ℕ} [hp : Fact p.Prime] (h : IsPGroup p G) : Group.IsNilpotent G

A p-group is nilpotent

theorem isNilpotent_of_product_of_sylow_group {G : Type u_1} [hG : Group G] [Fintype G] (e : ((p : { x : ℕ // x ∈ (Fintype.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G) : Group.IsNilpotent G

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

theorem isNilpotent_of_finite_tFAE {G : Type u_1} [hG : Group G] [Fintype G] : [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal, ∀ (p : ℕ), Fact p.Prime → ∀ (P : Sylow p G), P.Normal, Nonempty (((p : { x : ℕ // x ∈ (Fintype.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.