mathlib3
6c04fcf4 - refactor(group_theory/commutator): Use commutator notation in `commutator_normal` (#12575)

Commit

3 years ago

refactor(group_theory/commutator): Use commutator notation in `commutator_normal` (#12575) This PR uses the new commutator notation in the proof of `commutator_normal`.

Author

tb65536

Parents

84cbbc98

mathlib3 6c04fcf4 - refactor(group_theory/commutator): Use commutator notation in `commutator_normal` (#12575)

mathlib3
6c04fcf4 - refactor(group_theory/commutator): Use commutator notation in `commutator_normal` (#12575)