lTensor_zpow — Mathlib

English

Similarly, the right-tensor power of an automorphism on N satisfies (rTensor N f)^n = rTensor N (f^n).

Русский

Аналогично, правая тензорная степень отображения: (rTensor N f)^n = rTensor N (f^n).

LaTeX

$$$$(\\mathrm{rTensor} N\\; f)^n = \\mathrm{rTensor} N\\; f^n.$$$$

Lean4

@[simp]
theorem lTensor_zpow (f : N ≃ₗ[R] N) (n : ℤ) : f.lTensor M ^ n = (f ^ n).lTensor M := by
  simpa only [one_zpow] using TensorProduct.congr_zpow (1 : M ≃ₗ[R] M) f n

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