Theorems · Theorem · group theory

Subgroup.upperCentralSeries.eq_ge_of_eq_gt

∀ {G : Type u_1} [inst : Group G] {a b c : ℕ},
  a ≠ b →
    a ≤ c →
      Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b →
        Subgroup.upperCentralSeries G a = Subgroup.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.

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

1 results in Mathlib

Foundations

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

Assumes

Group