lTensor_pow — Mathlib

English

For a fixed M, the power of the left-tensor by an automorphism f on N satisfies (lTensor M f)^n = lTensor M (f^n).

Русский

Степень по умножению слева отобразит повторно: (lTensor M f)^n = lTensor M (f^n).

LaTeX

$$$$(\\mathrm{lTensor} M\\; f)^n = \\mathrm{lTensor} M\\; f^n.$$$$

Lean4

@[simp]
theorem lTensor_pow (f : N ≃ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lTensor M := by
  simpa only [one_pow] using TensorProduct.congr_pow (1 : M ≃ₗ[R] M) f n

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