Commit 2024-10-26 15:58 bf23ca54

View on Github →

feat: virtually nilpotent groups (#17628) Show that nilpotency is preserved under group isomorphisms and define virtually nilpotent subgroups. From GrowthInGroups

Estimated changes

Modified Mathlib/GroupTheory/Nilpotent.lean

added theorem Group.IsNilpotent.isVirtuallyNilpotent

modified theorem Group.IsNilpotent.nilpotent

added def Group.IsVirtuallyNilpotent

added theorem Group.isNilpotent_congr

added theorem Group.isNilpotent_top

added theorem comap_upperCentralSeries

modified theorem mem_upperCentralSeries_succ_iff