Theorems · Theorem · group theory

Subgroup.upperCentralSeriesAux.eq_def

∀ (G : Type u_1) [inst : Group G] (x : ℕ),
  Subgroup.upperCentralSeriesAux G x =
    match x with
    | 0 => ⟨⊥, ⋯⟩
    | n.succ =>
      let un := Subgroup.upperCentralSeriesAux G n;
      have _un_characteristic := ⋯;
      ⟨un.fst.upperCentralSeriesStep, ⋯⟩

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group