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

Commit

3 years ago

feat(group_theory/commutator): Add some basic lemmas (#12554) This PR adds lemmas adds some basic lemmas about when the commutator is trivial.

Author

tb65536

Parents