Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lower_central_series_one

Modification history

2022-02-18 19:21
src/group_theory/nilpotent.lean
refactor(group_theory/abelianization): Define `commutator` in terms of `general_commutator` (#11949) …
Modified lower_central_series_oneView on Github →
2022-01-22 13:06
src/group_theory/nilpotent.lean
feat(group_theory.nilpotent): add *_central_series_one G 1 = … simp lemmas (#11584) …
Added lower_central_series_oneView on Github →