Commit 2023-05-24 15:42 0372d31f
View on Github →feat(algebra/group/opposite): is_unit lemmas for mul_opposite (#19080)
I need these to build lemmas about right-multiplication by a unit out of lemmas about the left-action by a unit of the opposite ring, and this lets me convert that hypothesis.