mathlib3
f0dd6e9b - refactor(group_theory/commutator): Use commutators in `commutator_le` (#12572)

Commit

3 years ago

refactor(group_theory/commutator): Use commutators in `commutator_le` (#12572) This PR golfs the proof of `commutator_le`, and uses the new commutator notation.

Author

tb65536

Parents

6c04fcf4

mathlib3 f0dd6e9b - refactor(group_theory/commutator): Use commutators in `commutator_le` (#12572)

mathlib3
f0dd6e9b - refactor(group_theory/commutator): Use commutators in `commutator_le` (#12572)