feat(group_theory/commutator): Add some basic lemmas (#12554)
feat(group_theory/commutator): Add some basic lemmas (#12554)

This PR adds lemmas adds some basic lemmas about when the commutator is trivial.





leanprover-community/mathlib,leanprover-community/mathlib