rTensor_trans_congr — Mathlib

English

For f:P ≃ P', f:M ≃ P, g:N ≃ Q, the relation between rTensor and congrence holds: (f'.rTensor) ≪≫ TensorProduct.congr f g equals TensorProduct.congr (f' ≪≫ f) g.

Русский

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

LaTeX

$$$$(f' \\rTensor _ ) \\llcorner TensorProduct.congr f g = TensorProduct.congr (f' \\llcorner f) g.$$$$

Lean4

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

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