Mathlib v3 is deprecated. Go to Mathlib v4

Theorem comm_group.nilpotency_class_le_one

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.nilpotency_class_le_oneView on Github →