Theorem upperCentralSeries.StrictMonoOn

Modification history

2026-04-29 17:24

Mathlib/GroupTheory/Nilpotent.lean

chore(GroupTheory/Nilpotent): move declarations into namespace (#37175) …

Deleted upperCentralSeries.StrictMonoOn View on Github →

2026-03-17 11:27

Mathlib/GroupTheory/Nilpotent.lean

feat(GroupTheory/Nilpotent): remove `[IsNilpotent]` assumption from some theorems (#36093) …

Modified upperCentralSeries.StrictMonoOn View on Github →

2026-02-26 23:01

Mathlib/GroupTheory/Nilpotent.lean

feat: a nilpotent simple group is cyclic (#34318) …

Added upperCentralSeries.StrictMonoOn View on Github →