Theorems · Theorem · group theory

AddSubgroup.comap_upperCentralSeries_quotient_center

∀ {G : Type u_1} [inst : AddGroup G] (n : ℕ),
  AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.center G))
      (AddSubgroup.upperCentralSeries (G ⧸ AddSubgroup.center G) n) =
    AddSubgroup.upperCentralSeries G n.succ

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

AddGroupstatement and proof · cited by 4,410
AddSubgroupstatement and proof · cited by 3,232
HasQuotient.Quotientstatement and proof · cited by 2,301
AddSubgroup.comapstatement and proof · cited by 123
QuotientAddGroup.mk'statement and proof · cited by 60
symmproof · cited by 48
AddSubgroup.centerstatement and proof · cited by 40
AddSubgroup.upperCentralSeriesstatement and proof · cited by 32
QuotientAddGroup.ker_mk'proof · cited by 13
AddSubgroup.upperCentralSeries_oneproof · cited by 4
AddSubgroup.upperCentralSeriesStep_eq_comap_centerproof · cited by 1
QuotientAddGroup.comap_comap_centerproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

AddGroup.nilpotencyClass_quotient_centerproof · cited by 2
AddGroup.of_quotient_center_nilpotentproof · cited by 1