Theorems · Theorem · group theory

Group.nilpotencyClass_le_of_surjective

∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] (f : G →* G'),
  Function.Surjective ⇑f → ∀ [h : Group.IsNilpotent G], Group.nilpotencyClass G' ≤ Group.nilpotencyClass G

The nilpotency class of the range of a surjective homomorphism from a nilpotent group is less or equal the nilpotency class of the domain.

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupGroupGroup.IsNilpotent