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 characteristic 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 characteristic 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 ⊥.
• Group.nilpotencyClass : 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 Group.nilpotencyClass 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 Group.nilpotencyClass are provided.
• The Group.nilpotencyClass 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 Subgroup.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

• H.upperCentralSeriesStep = { carrier := {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

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

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

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

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

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

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

Equations

• Subgroup.upperCentralSeriesAux G 0 = ⟨⊥, ⋯⟩
• Subgroup.upperCentralSeriesAux G n.succ = ⟨(Subgroup.upperCentralSeriesAux G n).fst.upperCentralSeriesStep, ⋯⟩

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

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

This is the increasing chain of subgroups of G that starts with the trivial subgroup ⊥ of G and then continues defining upperCentralSeries G (n + 1) to be all the elements of G that, modulo upperCentralSeries G n, belong to the center of the quotient G ⧸ upperCentralSeries G n.

In particular, the identities

• upperCentralSeries G 0 = ⊥ (upperCentralSeries_zero);
• upperCentralSeries G 1 = center G (upperCentralSeries_one);

hold.

Equations

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

instance Subgroup.instCharacteristicUpperCentralSeries (G : Type u_1) [Group G] (n : ℕ) : (upperCentralSeries G n).Characteristic

@[simp]

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

@[simp]

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

theorem Subgroup.mem_upperCentralSeries_succ_iff {G : Type u_1} [Group G] {n : ℕ} {x : G} : x ∈ upperCentralSeries G (n + 1) ↔ ∀ (y : G), ⁅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.

@[simp]

theorem Subgroup.comap_upperCentralSeries {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : H ≃* G) (n : ℕ) : comap (↑e) (upperCentralSeries G n) = upperCentralSeries 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 : ℕ), Subgroup.upperCentralSeries G n = ⊤

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

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

theorem Group.isNilpotent_congr {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : G ≃* H) : IsNilpotent G ↔ IsNilpotent H

@[simp]

theorem Group.isNilpotent_top {G : Type u_1} [Group G] : IsNilpotent ↥⊤ ↔ IsNilpotent G

def Group.IsVirtuallyNilpotent (G : Type u_1) [Group G] : Prop

A group G is virtually nilpotent if it has a nilpotent cofinite subgroup N.

Equations

• Group.IsVirtuallyNilpotent G = ∃ (N : Subgroup G), Group.IsNilpotent ↥N ∧ N.FiniteIndex

theorem Group.IsNilpotent.isVirtuallyNilpotent {G : Type u_1} [Group G] (hG : IsNilpotent G) : IsVirtuallyNilpotent G

def Subgroup.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

• Subgroup.IsAscendingCentralSeries H = (H 0 = ⊥ ∧ ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n)

def Subgroup.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

• Subgroup.IsDescendingCentralSeries H = (H 0 = ⊤ ∧ ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1))

theorem Subgroup.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 Subgroup.upperCentralSeries_isAscendingCentralSeries (G : Type u_1) [Group G] : IsAscendingCentralSeries (upperCentralSeries G)

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

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

theorem Subgroup.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 Subgroup.is_descending_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 Subgroup.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 Subgroup.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 Subgroup.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

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

@[simp]

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

@[simp]

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

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

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

instance Subgroup.instCharacteristicLowerCentralSeries {G : Type u_1} [Group G] (n : ℕ) : (lowerCentralSeries G n).Characteristic

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

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

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

theorem Subgroup.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 Subgroup.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] : ℕ

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. If G is not nilpotent then the nilpotency class takes the junk value 0.

Equations

• Group.nilpotencyClass G = if hG : Group.IsNilpotent G then Nat.find ⋯ else 0

theorem Group.nilpotencyClass_of_not_nilpotent {G : Type u_1} [Group G] (hG : ¬IsNilpotent G) : nilpotencyClass G = 0

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

@[simp]

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

theorem Subgroup.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 Subgroup.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 Subgroup.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 Subgroup.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 Subgroup.lowerCentralSeries_nilpotencyClass {G : Type u_1} [Group G] [hG : Group.IsNilpotent G] : lowerCentralSeries G (Group.nilpotencyClass G) = ⊥

theorem Subgroup.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 Subgroup.lowerCentralSeries_map_subtype_le {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : 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

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] : IsNilpotent G

theorem Subgroup.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 Subgroup.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 Subgroup.lowerCentralSeries_succ_eq_bot {G : Type u_1} [Group G] {n : ℕ} (h : lowerCentralSeries G n ≤ center G) : lowerCentralSeries G (n + 1) = ⊥

theorem Subgroup.isNilpotent_of_ker_le_center {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (hf1 : f.ker ≤ center G) [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 Group.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) [IsNilpotent H] : nilpotencyClass G ≤ nilpotencyClass H + 1

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

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

theorem Group.nilpotencyClass_le_of_surjective {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] (f : G →* G') (hf : Function.Surjective ⇑f) [h : IsNilpotent G] : nilpotencyClass G' ≤ 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 Group.nilpotent_of_mulEquiv {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] [_h : IsNilpotent G] (f : G ≃* G') : IsNilpotent G'

Nilpotency respects isomorphisms

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

A quotient of a nilpotent group is nilpotent

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

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

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

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

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

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

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

Quotienting the center G reduces the nilpotency class by 1

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

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

theorem Group.nilpotent_center_quotient_ind {P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop} (G : Type u_2) [Group G] [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 : 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 Subgroup.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

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

Abelian groups have nilpotency class at most one

@[implicit_reducible]

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 Subgroup.upperCentralSeries.eq_ge_of_eq_succ {G : Type u_1} [Group G] {a b : ℕ} (ab : a ≤ b) (hn : upperCentralSeries G a = upperCentralSeries G (a + 1)) : upperCentralSeries G a = upperCentralSeries G b

theorem Subgroup.upperCentralSeries.eq_ge_of_eq_gt {G : Type u_1} [Group G] {a b c : ℕ} (ab : a < b) (ac : a ≤ c) (hn : upperCentralSeries G a = upperCentralSeries G b) : upperCentralSeries G a = upperCentralSeries G c

If two different elements of the upperCentralSeries of a group G are equal, then they are all equal, starting from the smaller index.

theorem Subgroup.upperCentralSeries.eq_top {G : Type u_1} [Group G] [Group.IsNilpotent G] {a b : ℕ} (ab : a < b) (hn : upperCentralSeries G a = upperCentralSeries G b) : upperCentralSeries G a = ⊤

theorem Subgroup.nilpotencyClass_le_of_upperCentralSeries_eq {G : Type u_1} [Group G] {a b : ℕ} (ab : a < b) (hn : upperCentralSeries G a = upperCentralSeries G b) : Group.nilpotencyClass G ≤ a

theorem Subgroup.upperCentralSeries.StrictMonoOn (G : Type u_1) [Group G] : _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (Group.nilpotencyClass G))

theorem Subgroup.upperCentralSeries.card_image_eq_of_le_nilpotencyClass {G : Type u_1} [Group G] {a : ℕ} (h2 : a ≤ Group.nilpotencyClass G) : (upperCentralSeries G '' Set.Iic a).ncard = a + 1

theorem Subgroup.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 Group.isNilpotent_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [IsNilpotent G₁] [IsNilpotent G₂] : IsNilpotent (G₁ × G₂)

Products of nilpotent groups are nilpotent

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

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

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

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

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

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

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

n-ary products of nilpotent groups are nilpotent

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

@[implicit_reducible]

instance instCommGroupOfIsSimpleGroupOfIsNilpotent {G : Type u_1} [Group G] [IsSimpleGroup G] [Group.IsNilpotent G] : CommGroup G

Equations

• instCommGroupOfIsSimpleGroupOfIsNilpotent = { toGroup := inst✝², mul_comm := ⋯ }

instance instIsCyclicOfIsSimpleGroupOfIsNilpotent {G : Type u_1} [Group G] [IsSimpleGroup G] [Group.IsNilpotent G] : IsCyclic G

theorem Group.nilpotencyClass_le_one_of_isSimple_of_isNilpotent {G : Type u_1} [Group G] [IsSimpleGroup G] [IsNilpotent G] : nilpotencyClass G ≤ 1

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

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

A p-group is nilpotent

theorem Group.isNilpotent_of_product_of_sylow_group {G : Type u_1} [hG : Group G] [Finite G] (e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G) : IsNilpotent G

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

theorem Group.isNilpotent_of_finite_tfae {G : Type u_1} [hG : Group G] [Finite G] : [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.

@[deprecated Subgroup.upperCentralSeriesStep (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeriesStep.

---

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 = @Subgroup.upperCentralSeriesStep

@[deprecated Subgroup.mem_upperCentralSeriesStep (since := "2026-03-25")]

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

Alias of Subgroup.mem_upperCentralSeriesStep.

@[deprecated Subgroup.upperCentralSeriesStep_eq_comap_center (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeriesStep_eq_comap_center.

---

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

@[deprecated Subgroup.upperCentralSeriesAux (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeriesAux.

---

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

Equations

• upperCentralSeriesAux = Subgroup.upperCentralSeriesAux

@[deprecated Subgroup.upperCentralSeries (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeries.

---

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

This is the increasing chain of subgroups of G that starts with the trivial subgroup ⊥ of G and then continues defining upperCentralSeries G (n + 1) to be all the elements of G that, modulo upperCentralSeries G n, belong to the center of the quotient G ⧸ upperCentralSeries G n.

In particular, the identities

• upperCentralSeries G 0 = ⊥ (upperCentralSeries_zero);
• upperCentralSeries G 1 = center G (upperCentralSeries_one);

hold.

Equations

• upperCentralSeries = Subgroup.upperCentralSeries

@[deprecated Subgroup.upperCentralSeries_zero (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeries_zero.

@[deprecated Subgroup.upperCentralSeries_one (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeries_one.

@[deprecated Subgroup.mem_upperCentralSeries_succ_iff (since := "2026-03-25")]

theorem mem_upperCentralSeries_succ_iff {G : Type u_1} [Group G] {n : ℕ} {x : G} : x ∈ Subgroup.upperCentralSeries G (n + 1) ↔ ∀ (y : G), ⁅x, y⁆ ∈ Subgroup.upperCentralSeries G n

Alias of Subgroup.mem_upperCentralSeries_succ_iff.

---

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

@[deprecated Subgroup.comap_upperCentralSeries (since := "2026-03-25")]

theorem comap_upperCentralSeries {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : H ≃* G) (n : ℕ) : Subgroup.comap (↑e) (Subgroup.upperCentralSeries G n) = Subgroup.upperCentralSeries H n

Alias of Subgroup.comap_upperCentralSeries.

@[deprecated Subgroup.IsAscendingCentralSeries (since := "2026-03-25")]

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

Alias of Subgroup.IsAscendingCentralSeries.

---

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 = @Subgroup.IsAscendingCentralSeries

@[deprecated Subgroup.IsDescendingCentralSeries (since := "2026-03-25")]

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

Alias of Subgroup.IsDescendingCentralSeries.

---

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 = @Subgroup.IsDescendingCentralSeries

@[deprecated Subgroup.ascending_central_series_le_upper (since := "2026-03-25")]

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

Alias of Subgroup.ascending_central_series_le_upper.

---

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

@[deprecated Subgroup.upperCentralSeries_isAscendingCentralSeries (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeries_isAscendingCentralSeries.

---

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

@[deprecated Subgroup.upperCentralSeries_mono (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeries_mono.

@[deprecated Subgroup.nilpotent_iff_finite_ascending_central_series (since := "2026-03-25")]

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

Alias of Subgroup.nilpotent_iff_finite_ascending_central_series.

---

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

@[deprecated Subgroup.is_descending_rev_series_of_is_ascending (since := "2026-03-25")]

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

Alias of Subgroup.is_descending_rev_series_of_is_ascending.

@[deprecated Subgroup.is_ascending_rev_series_of_is_descending (since := "2026-03-25")]

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

Alias of Subgroup.is_ascending_rev_series_of_is_descending.

@[deprecated Subgroup.nilpotent_iff_finite_descending_central_series (since := "2026-03-25")]

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

Alias of Subgroup.nilpotent_iff_finite_descending_central_series.

---

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

@[deprecated Subgroup.lowerCentralSeries (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries.

---

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 = Subgroup.lowerCentralSeries

@[deprecated Subgroup.lowerCentralSeries_zero (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_zero.

@[deprecated Subgroup.lowerCentralSeries_one (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_one.

@[deprecated Subgroup.mem_lowerCentralSeries_succ_iff (since := "2026-03-25")]

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

Alias of Subgroup.mem_lowerCentralSeries_succ_iff.

@[deprecated Subgroup.lowerCentralSeries_succ (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_succ.

@[deprecated Subgroup.lowerCentralSeries_antitone (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_antitone.

@[deprecated Subgroup.lowerCentralSeries_isDescendingCentralSeries (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_isDescendingCentralSeries.

---

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

@[deprecated Subgroup.descending_central_series_ge_lower (since := "2026-03-25")]

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

Alias of Subgroup.descending_central_series_ge_lower.

---

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

@[deprecated Subgroup.nilpotent_iff_lowerCentralSeries (since := "2026-03-25")]

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

Alias of Subgroup.nilpotent_iff_lowerCentralSeries.

---

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

@[deprecated Subgroup.upperCentralSeries_nilpotencyClass (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeries_nilpotencyClass.

@[deprecated Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le (since := "2026-03-25")]

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

Alias of Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le.

@[deprecated Subgroup.least_ascending_central_series_length_eq_nilpotencyClass (since := "2026-03-25")]

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

Alias of Subgroup.least_ascending_central_series_length_eq_nilpotencyClass.

---

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.

@[deprecated Subgroup.least_descending_central_series_length_eq_nilpotencyClass (since := "2026-03-25")]

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

Alias of Subgroup.least_descending_central_series_length_eq_nilpotencyClass.

---

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.

@[deprecated Subgroup.lowerCentralSeries_length_eq_nilpotencyClass (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_length_eq_nilpotencyClass.

---

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

@[deprecated Subgroup.lowerCentralSeries_nilpotencyClass (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_nilpotencyClass.

@[deprecated Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.

@[deprecated Subgroup.lowerCentralSeries_map_subtype_le (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_map_subtype_le.

@[deprecated Subgroup.upperCentralSeries.map (since := "2026-03-25")]

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 (Subgroup.upperCentralSeries G n) ≤ Subgroup.upperCentralSeries H n

Alias of Subgroup.upperCentralSeries.map.

@[deprecated Subgroup.lowerCentralSeries.map (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries.map.

@[deprecated Subgroup.lowerCentralSeries_succ_eq_bot (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_succ_eq_bot.

@[deprecated Subgroup.isNilpotent_of_ker_le_center (since := "2026-03-25")]

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) [Group.IsNilpotent H] : Group.IsNilpotent G

Alias of Subgroup.isNilpotent_of_ker_le_center.

---

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

@[deprecated Group.nilpotencyClass_le_of_ker_le_center (since := "2026-03-25")]

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) [Group.IsNilpotent H] : Group.nilpotencyClass G ≤ Group.nilpotencyClass H + 1

Alias of Group.nilpotencyClass_le_of_ker_le_center.

@[deprecated Group.nilpotent_of_surjective (since := "2026-03-25")]

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'

Alias of Group.nilpotent_of_surjective.

---

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

@[deprecated Group.nilpotencyClass_le_of_surjective (since := "2026-03-25")]

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

Alias of Group.nilpotencyClass_le_of_surjective.

---

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

@[deprecated Group.nilpotent_of_mulEquiv (since := "2026-03-25")]

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'

Alias of Group.nilpotent_of_mulEquiv.

---

Nilpotency respects isomorphisms

@[deprecated Group.nilpotent_quotient_of_nilpotent (since := "2026-03-25")]

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

Alias of Group.nilpotent_quotient_of_nilpotent.

---

A quotient of a nilpotent group is nilpotent

@[deprecated Group.nilpotencyClass_quotient_le (since := "2026-03-25")]

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

Alias of Group.nilpotencyClass_quotient_le.

---

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

@[deprecated Subgroup.comap_upperCentralSeries_quotient_center (since := "2026-03-25")]

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

Alias of Subgroup.comap_upperCentralSeries_quotient_center.

@[deprecated Group.nilpotencyClass_zero_iff_subsingleton (since := "2026-03-25")]

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

Alias of Group.nilpotencyClass_zero_iff_subsingleton.

@[deprecated Group.of_quotient_center_nilpotent (since := "2026-03-25")]

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

Alias of Group.of_quotient_center_nilpotent.

---

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

@[deprecated Group.nilpotencyClass_quotient_center (since := "2026-03-25")]

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

Alias of Group.nilpotencyClass_quotient_center.

---

Quotienting the center G reduces the nilpotency class by 1

@[deprecated Group.nilpotencyClass_eq_quotient_center_plus_one (since := "2026-03-25")]

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

Alias of Group.nilpotencyClass_eq_quotient_center_plus_one.

---

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

@[deprecated Group.nilpotent_center_quotient_ind (since := "2026-03-25")]

theorem nilpotent_center_quotient_ind {P : (G : Type u_2) → [inst : Group G] → [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

Alias of Group.nilpotent_center_quotient_ind.

---

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.

@[deprecated Subgroup.derived_le_lower_central (since := "2026-03-25")]

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

Alias of Subgroup.derived_le_lower_central.

@[deprecated Subgroup.upperCentralSeries.eq_ge_of_eq_succ (since := "2026-03-25")]

theorem upperCentralSeries.eq_ge_of_eq_succ {G : Type u_1} [Group G] {a b : ℕ} (ab : a ≤ b) (hn : Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G (a + 1)) : Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b

Alias of Subgroup.upperCentralSeries.eq_ge_of_eq_succ.

@[deprecated Subgroup.upperCentralSeries.eq_ge_of_eq_gt (since := "2026-03-25")]

theorem upperCentralSeries.eq_ge_of_eq_gt {G : Type u_1} [Group G] {a b c : ℕ} (ab : a < b) (ac : a ≤ c) (hn : Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b) : Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G c

Alias of Subgroup.upperCentralSeries.eq_ge_of_eq_gt.

---

If two different elements of the upperCentralSeries of a group G are equal, then they are all equal, starting from the smaller index.

@[deprecated Subgroup.upperCentralSeries.eq_top (since := "2026-03-25")]

theorem upperCentralSeries.eq_top {G : Type u_1} [Group G] [Group.IsNilpotent G] {a b : ℕ} (ab : a < b) (hn : Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b) : Subgroup.upperCentralSeries G a = ⊤

Alias of Subgroup.upperCentralSeries.eq_top.

@[deprecated Subgroup.nilpotencyClass_le_of_upperCentralSeries_eq (since := "2026-03-25")]

theorem nilpotencyClass_le_of_upperCentralSeries_eq {G : Type u_1} [Group G] {a b : ℕ} (ab : a < b) (hn : Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b) : Group.nilpotencyClass G ≤ a

Alias of Subgroup.nilpotencyClass_le_of_upperCentralSeries_eq.

@[deprecated Subgroup.upperCentralSeries.StrictMonoOn (since := "2026-03-25")]

theorem upperCentralSeries.StrictMonoOn (G : Type u_1) [Group G] : _root_.StrictMonoOn (Subgroup.upperCentralSeries G) (Set.Iic (Group.nilpotencyClass G))

Alias of Subgroup.upperCentralSeries.StrictMonoOn.

@[deprecated Subgroup.upperCentralSeries.card_image_eq_of_le_nilpotencyClass (since := "2026-03-25")]

theorem upperCentralSeries.card_image_eq_of_le_nilpotencyClass {G : Type u_1} [Group G] {a : ℕ} (h2 : a ≤ Group.nilpotencyClass G) : (Subgroup.upperCentralSeries G '' Set.Iic a).ncard = a + 1

Alias of Subgroup.upperCentralSeries.card_image_eq_of_le_nilpotencyClass.

@[deprecated Subgroup.lowerCentralSeries_prod (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_prod.

@[deprecated Group.isNilpotent_prod (since := "2026-03-25")]

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

Alias of Group.isNilpotent_prod.

---

Products of nilpotent groups are nilpotent

@[deprecated Group.nilpotencyClass_prod (since := "2026-03-25")]

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₂)

Alias of Group.nilpotencyClass_prod.

---

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

@[deprecated Subgroup.lowerCentralSeries_pi_le (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_pi_le.

@[deprecated Group.isNilpotent_pi_of_bounded_class (since := "2026-03-25")]

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)

Alias of Group.isNilpotent_pi_of_bounded_class.

---

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

@[deprecated Subgroup.lowerCentralSeries_pi_of_finite (since := "2026-03-25")]

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

Alias of Subgroup.lowerCentralSeries_pi_of_finite.

@[deprecated Group.isNilpotent_pi (since := "2026-03-25")]

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

Alias of Group.isNilpotent_pi.

---

n-ary products of nilpotent groups are nilpotent

@[deprecated Group.nilpotencyClass_pi (since := "2026-03-25")]

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)

Alias of Group.nilpotencyClass_pi.

---

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

@[deprecated Group.nilpotencyClass_le_one_of_isSimple_of_isNilpotent (since := "2026-03-25")]

theorem nilpotencyClass_le_one_of_isSimple_of_isNilpotent {G : Type u_1} [Group G] [IsSimpleGroup G] [Group.IsNilpotent G] : Group.nilpotencyClass G ≤ 1

Alias of Group.nilpotencyClass_le_one_of_isSimple_of_isNilpotent.

@[deprecated Group.normalizerCondition_of_isNilpotent (since := "2026-03-25")]

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

Alias of Group.normalizerCondition_of_isNilpotent.

@[deprecated Group.isNilpotent_of_product_of_sylow_group (since := "2026-03-25")]

theorem isNilpotent_of_product_of_sylow_group {G : Type u_1} [hG : Group G] [Finite G] (e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G) : Group.IsNilpotent G

Alias of Group.isNilpotent_of_product_of_sylow_group.

---

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

@[deprecated Group.isNilpotent_of_finite_tfae (since := "2026-03-25")]

theorem 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

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.