Theorems · Theorem · group theory

Subgroup.upperCentralSeriesStep.hcongr_4

∀ (G G' : Type u_1),
  G = G' →
    ∀ (inst : Group G) (inst' : Group G'),
      inst ≍ inst' →
        ∀ (N : Subgroup G) (N' : Subgroup G'),
          N ≍ N' →
            ∀ (inst_1 : N.Normal) (inst'_1 : N'.Normal),
              inst_1 ≍ inst'_1 → N.upperCentralSeriesStep ≍ N'.upperCentralSeriesStep

Defined in: Mathlib.GroupTheory.Nilpotent
Cited by: 0 results in Mathlib
Foundations: Depth 41 from the axioms · uses propext

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 and proof · cited by 3,593
Subgroup.Normalstatement and proof · cited by 334
Subgroup.upperCentralSeriesStepstatement and proof · cited by 8

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.