mathlib
504e1f60 - feat(group_theory.nilpotent): add *_central_series_one G 1 = … simp lemmas (#11584)

Commit

3 years ago

feat(group_theory.nilpotent): add *_central_series_one G 1 = … simp lemmas (#11584) analogously to the existing `_zero` lemmas

Author

nomeata

Parents