Commit 2022-01-22 13:06 504e1f60
View on Github →feat(group_theory.nilpotent): add *_central_series_one G 1 = … simp lemmas (#11584)
analogously to the existing _zero lemmas
feat(group_theory.nilpotent): add *_central_series_one G 1 = … simp lemmas (#11584)
analogously to the existing _zero lemmas