rTensor_pow — Mathlib

English

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

Русский

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

LaTeX

$$$$(\\mathrm{TensorProduct.congr} f g) \\trans (f' \\rTensor Q) = \\mathrm{TensorProduct.congr} (f \\trans f') g.$$$$

Lean4

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

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