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.

Estimated changes

added theorem is_unit.op
added theorem is_unit.unop
added theorem is_unit_op
added theorem is_unit_unop