Theorems · Theorem · group theory

AddSubgroup.isNilpotent_of_ker_le_center

∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (f : G →+ H),
  f.ker ≤ AddSubgroup.center G → ∀ [AddGroup.IsNilpotent H], AddGroup.IsNilpotent G

The preimage of a nilpotent additive group is nilpotent if the kernel of the homomorphism is contained in the center.

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddGroup.IsNilpotent