map_op_pow — Mathlib

English

If you map powers of a submodule using the opposite-structure linear map, you get the power of the mapped submodule.

Русский

Если отображать степени подмодуля через линейное отображение, соответствующее противоположному структурам, получается степень образа.

LaTeX

$$$\mathrm{map}(\mathrm{opLinearEquiv}_R)^{\mathrm{toLinearMap}}(\mathrm{M}^{n}) = (\mathrm{map}(\mathrm{opLinearEquiv}_R)^{\mathrm{toLinearMap}}\mathrm{M})^{n}$$$

Lean4

theorem map_op_pow (n : ℕ) :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n :=
  by rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]

Похожие утверждения