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
simp
s here, that I had to massage withsimp only
and more. I didn't expect these to be so slow. - I had to add a shortcut instance for
MulAction (ConjAct G) G
in order for TC inference to find it in the declarationstabilizer_eq_centralizer
. - There were several
simp
lemmas thatsimpNF
said it could prove for which I just removed thesimp
attribute. I think we may at least want to consider addressing the first two problems before merging.