# 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.