rTensor_zpow — Mathlib

English

For g' : Q ≃ S, f : M ≃ P, g : N ≃ Q, the equality (TensorProduct.congr f g) trans (g' lTensor _) equals (TensorProduct.congr f (g trans g')).

Русский

Для g' , f и g выполняется: (congr f g) trans (g' lTensor _) = congr f (g trans g').

LaTeX

$$$$(\\mathrm{TensorProduct.congr} f g) \\trans (g' \\lTensor P) = \\mathrm{TensorProduct.congr} f (g \\trans g').$$$$

Lean4

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

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