Mathlib v3 is deprecated. Go to Mathlib v4

Theorem upper_central_series_one

Modification history

2022-01-22 13:06
src/group_theory/nilpotent.lean
feat(group_theory.nilpotent): add *_central_series_one G 1 = … simp lemmas (#11584) …
Added upper_central_series_oneView on Github →