Commit 2022-02-18 19:21 ffc2bdfb

View on Github →

refactor(group_theory/abelianization): Define commutator in terms of general_commutator (#11949) It seems reasonable to define commutator in terms of general_commutator.

Estimated changes

Modified src/group_theory/abelianization.lean

added theorem commutator_def

added theorem commutator_eq_closure

added theorem commutator_eq_normal_closure

Modified src/group_theory/nilpotent.lean

modified theorem lower_central_series_one

Modified src/group_theory/solvable.lean

deleted theorem commutator_def'

deleted theorem general_commutator_eq_commutator