mathlib
3d41a5bd - refactor(group_theory/commutator): Golf proof of `commutator_mono` (#12619)

Commit

4 years ago

refactor(group_theory/commutator): Golf proof of `commutator_mono` (#12619) This PR golfs the proof of `commutator_mono` by using `commutator_le` rather than `closure_mono`.

Author

tb65536

Parents

72c6979b

mathlib 3d41a5bd - refactor(group_theory/commutator): Golf proof of `commutator_mono` (#12619)

mathlib
3d41a5bd - refactor(group_theory/commutator): Golf proof of `commutator_mono` (#12619)