Commit 2022-03-03 00:08 9deeddb3

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.