Mathlib v3 is deprecated. Go to Mathlib v4

Def group.comm_group_of_center_eq_top

Modification history

2022-01-31 15:42

src/group_theory/subgroup/basic.lean

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

Added group.comm_group_of_center_eq_top View on Github →