Theorems · Theorem · group theory

Subgroup.upperCentralSeries.eq_ge_of_eq_succ

∀ {G : Type u_1} [inst : Group G] {a b : ℕ},
  a ≤ b →
    Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G (a + 1) →
      Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b

Defined in: Mathlib.GroupTheory.Nilpotent
Cited by: 3 results in Mathlib
Foundations: Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Groupstatement and proof · cited by 6,238
Subgroupstatement · cited by 3,593
Subgroup.upperCentralSeriesstatement and proof · cited by 51
Nat.le_inductionproof · cited by 46

Cited by3

Results whose statement or proof uses this declaration.

Subgroup.upperCentralSeries.eq_ge_of_eq_gtproof · cited by 1
Group.IsPerfect.upperCentralSeries_eq_centerproof · cited by 1
upperCentralSeries.eq_ge_of_eq_succproof · cited by 0