English
Transporting submodules via the opposite-linear equivalence preserves powers: comap (opLinearEquiv R).toLinearMap (M^n) = comap (opLinearEquiv R).toLinearMap M^n.
Русский
Перенос подмодулей через обратное линейное эквивалентное отображение сохраняет степени: comap (opLinearEquiv R).toLinearMap (M^n) = comap (opLinearEquiv R).toLinearMap M^n.
LaTeX
$$$\mathrm{comap}(\mathrm{opLinearEquiv}_R .\mathrm{toLinearMap})(\mathrm{M}^{n}) = \mathrm{comap}(\mathrm{opLinearEquiv}_R .\mathrm{toLinearMap})(\mathrm{M})^{n}$$$
Lean4
theorem comap_op_pow (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n :=
op_injective <| (equivOpposite : Submodule R Aᵐᵒᵖ ≃+* _).map_pow M n
