mathlib3

0372d31f - feat(algebra/group/opposite): `is_unit` lemmas for `mul_opposite` (#19080)

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.