congr_trans_lTensor — Mathlib

English

For f : M ≃ P, g : N ≃ Q and g' : S ≃ N, the equality g'.lTensor _ ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g) holds.

Русский

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

LaTeX

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

Lean4

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

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