pow_toLinearMap — Mathlib

English

If σ is an algebra automorphism of A1 over R, then the linear map associated to σ^n is the nth power of the linear map associated to σ.

Русский

Если σ — алгебраический автоморфизм A1 над R, то линейное отображение, соответствующее σ^n, равно n-й степени линейного отображения, соответствующего σ.

LaTeX

$$$ (\\sigma^n)^{\\,\\mathrm{toLinearMap}} = (\\sigma^{\\mathrm{toLinearMap}})^n. $$$

Lean4

theorem pow_toLinearMap (σ : A₁ ≃ₐ[R] A₁) (n : ℕ) : (σ ^ n).toLinearMap = σ.toLinearMap ^ n :=
  (AlgEquiv.toLinearMapHom R A₁).map_pow σ n

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