Commit 2023-01-27 09:47 34bf5453
View on Github →feat: port GroupTheory.GroupAction.ConjAct (#1871) This compiles and lints now, BUT...
- There were some very slow
simps here, that I had to massage withsimp onlyand more. I didn't expect these to be so slow. - I had to add a shortcut instance for
MulAction (ConjAct G) Gin order for TC inference to find it in the declarationstabilizer_eq_centralizer. - There were several
simplemmas thatsimpNFsaid it could prove for which I just removed thesimpattribute. I think we may at least want to consider addressing the first two problems before merging.