Commit 2023-01-27 09:47 34bf5453

View on Github →

feat: port GroupTheory.GroupAction.ConjAct (#1871) This compiles and lints now, BUT...

  1. There were some very slow simps here, that I had to massage with simp only and more. I didn't expect these to be so slow.
  2. I had to add a shortcut instance for MulAction (ConjAct G) G in order for TC inference to find it in the declaration stabilizer_eq_centralizer.
  3. There were several simp lemmas that simpNF said it could prove for which I just removed the simp attribute. I think we may at least want to consider addressing the first two problems before merging.

Estimated changes