Commit 2023-01-26 16:39 d72dc50d

View on Github →

feat: port GroupTheory.Subgroup.MulOpposite (#1857) porting notes:

  1. the H.opposite notation isn't working, which I think is due to the fact that subgroup.opposite is an equiv and Lean doesn't find the CoeFun instance. I think I saw something on Zulip about this, but I can't find it. I'm not sure if there is a resolution; to get it working I just wrote opposite H instead of H.opposite
  2. the simp call at the end was broken, I think because it didn't rewrite the scalar multiplication by the opposite element as multiplication on the right, so I just golfed it.

Estimated changes