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 : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ map (↑(LinearEquiv.symm (opLinearEquiv R))) (M ^ n) = map (↑(LinearEquiv.symm (opLinearEquiv R))) M ^ n
rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]