lTensor_trans_rTensor — Mathlib

English

For linear isomorphisms f,g and a third isomorphism f', the composition (f'.rTensor) trans (TensorProduct.congr f g) equals TensorProduct.congr (f' trans f) g.

Русский

Для линейных изоморфизмов f, g и f' композиция (f'.rTensor) ⋅ (congr f g) равна congr f' f по g.

LaTeX

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

Lean4

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

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