Commit 2022-01-05 12:21 cef32586

chore(group_theory/group_action/defs): add instances to copy statements about left actions to right actions when the two are equal (#10949) While these instances are usually available elsewhere, these shortcuts can reduce the number of typeclass assumptions other lemmas needs. Since the instances carry no data, the only harm they can cause is performance. There were some typeclass loops brought on by some bad instance unification, similar to the ones removed by @Vierkantor in 9ee2a50aa439d092c8dea16c1f82f7f8e1f1ea2c. We turn these into lemmas and duplicate the docstring explaining the problem. That commit has a much longer explanation of the problem.