mathlib

9deeddb3 - feat(algebra/algebra/operations): `submodule.map_pow` and opposite lemmas (#12374)

feat(algebra/algebra/operations): `submodule.map_pow` and opposite lemmas (#12374) To prove `map_pow`, we add `submodule.map_hom` to match the very-recently-added `ideal.map_hom`. The opposite lemmas can be used to extend these results for maps that reverse multiplication, by factoring them into an `alg_hom` into the opposite type composed with `mul_opposite.op`. `(↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ)` is really a mouthful, but the elaborator can't seem to work out the type any other way, and `.to_linear_map` appears not to be the preferred form for `simp` lemmas.