map_pow — Mathlib

English

Taking comaps along the opposite-structure linear equivalence commutes with taking powers of Submodules: comap (opLinearEquiv R).symm (M^n) = comap (opLinearEquiv R).symm M^n.

Русский

Сопоставление через обратную структуру линейного эквивалента commuting с возведением подмодулей в степень: comap (opLinearEquiv R).symm (M^n) = comap (opLinearEquiv R).symm M^n.

LaTeX

$$$\mathrm{comap}( (\mathrm{opLinearEquiv}^R)^{-1} , M^n) = \mathrm{comap}( (\mathrm{opLinearEquiv}^R)^{-1} , M)^n$$$

Lean4

protected theorem map_pow {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (n : ℕ) :
    map f.toLinearMap (M ^ n) = map f.toLinearMap M ^ n :=
  map_pow (mapHom f) M n

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