mathlib3

0ec8e6a0 - feat(algebra/algebra/operations): more lemmas about `mul_opposite` (#12441)

feat(algebra/algebra/operations): more lemmas about `mul_opposite` (#12441) Naturally the lemmas I left out of the previous PR, notably `map_unop_mul` and `map_unop_pow`, are the ones I actually needed. This also improves the `simps` lemmas on `submodule.equiv_opposite`, which were previously garbage as `simps` didn't unfold `ring_equiv.symm` properly. At any rate, the only reason it was defined that way was because the lemmas in this PR were missing.