Theorems · Theorem · group theory

Subgroup.comap_upperCentralSeries_quotient_center

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

Defined in: Mathlib.GroupTheory.Nilpotent
Cited by: 3 results in Mathlib
Foundations: Depth 91 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.

Cites12

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
HasQuotient.Quotientstatement and proof · cited by 2,301
Subgroup.comapstatement and proof · cited by 154
Subgroup.centerstatement and proof · cited by 121
QuotientGroup.mk'statement and proof · cited by 90
Subgroup.upperCentralSeriesstatement and proof · cited by 51
symmproof · cited by 48
QuotientGroup.ker_mk'proof · cited by 18
Subgroup.upperCentralSeries_oneproof · cited by 7
Subgroup.upperCentralSeriesStep_eq_comap_centerproof · cited by 2
QuotientGroup.comap_comap_centerproof · cited by 1

Cited by3

Results whose statement or proof uses this declaration.

Group.nilpotencyClass_quotient_centerproof · cited by 3
comap_upperCentralSeries_quotient_centerproof · cited by 0
Group.IsPerfect.center_quotient_center_eq_botproof · cited by 0