Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 15:42 76b2a0ec

View on Github →

feat(group_theory/nilpotent): abelian iff nilpotency class ≤ 1 (#11718)

Estimated changes

Modified src/group_theory/nilpotent.lean

added theorem comm_group.nilpotency_class_le_one

added def comm_group_of_nilpotency_class

Modified src/group_theory/subgroup/basic.lean

added theorem comm_group.center_eq_top

added def group.comm_group_of_center_eq_top