-
Notifications
You must be signed in to change notification settings - Fork 298
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(group_theory/group_action/defs): add instances to copy statemen…
…ts 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 9ee2a50. We turn these into `lemma`s and duplicate the docstring explaining the problem. That commit has a much longer explanation of the problem.
- Loading branch information
1 parent
8d5830e
commit cef3258
Showing
1 changed file
with
36 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters