mathlib3
ffc2bdfb - refactor(group_theory/abelianization): Define `commutator` in terms of `general_commutator` (#11949)

Commit

3 years ago

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

Author

tb65536

Parents

018c7289

mathlib3 ffc2bdfb - refactor(group_theory/abelianization): Define `commutator` in terms of `general_commutator` (#11949)

mathlib3
ffc2bdfb - refactor(group_theory/abelianization): Define `commutator` in terms of `general_commutator` (#11949)