Commit 2023-01-26 16:39 d72dc50d
View on Github →feat: port GroupTheory.Subgroup.MulOpposite (#1857) porting notes:
- the
H.opposite
notation isn't working, which I think is due to the fact thatsubgroup.opposite
is an equiv and Lean doesn't find theCoeFun
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 wroteopposite H
instead ofH.opposite
- 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.