rTensor_trans_lTensor — Mathlib

English

For linear isomorphisms f:M≃P and g:N≃Q, the canonical tensor-product isomorphism f.rTensor N followed by g.lTensor P equals TensorProduct.congr f g.

Русский

Для линейных изоморфизмов f: M ≃ P и g: N ≃ Q каноническое тензорно-изоморфизмом f.rTensor N, затем g.lTensor P, равно TensorProduct.congr f g.

LaTeX

$$$$(f.rTensor N) \\; \\llcorner \\; g.lTensor P = \\mathrm{TensorProduct.congr}(f,g).$$$$

Lean4

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

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