no goals
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
⊢ map (↑(opLinearEquiv R)) (M ^ n) = map (↑(opLinearEquiv R)) M ^ n
rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]