Def comm_group_of_nilpotency_class

Modification history

2022-01-31 15:42
src/group_theory/nilpotent.lean
feat(group_theory/nilpotent): abelian iff nilpotency class ≤ 1 (#11718)
Added comm_group_of_nilpotency_classView on Github →