mathlib

20c520a6 - feat(algebra/opposite): inversion is a mul_equiv to the opposite group (#7330)

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.