Commit 2021-04-27 07:21 20c520a6

feat(algebra/opposite): inversion is a mul_equiv to the opposite group (#7330) This also splits out monoid_hom.to_opposite from ring_hom.to_opposite, and adds add_equiv.neg and mul_equiv.inv for the case when the (add_)group is commutative.