lTensor_trans_congr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lTensor_trans_congr (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (g' : S ≃ₗ[R] N) :
    g'.lTensor _ ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g) :=
  toLinearMap_injective <| LinearMap.map_comp_lTensor M _ _ _

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