map_rTensor — Mathlib

English

Another composition identity: (f.rTensor Q).comp (g.lTensor M) equals TensorProduct.map f g.

Русский

Ещё одно тождество композиции: (f.rTensor Q).comp (g.lTensor M) = TensorProduct.map f g.

LaTeX

$$$(f.rTensor Q).\mathrm{comp} (g.lTensor M) = \mathrm{TensorProduct}.map f g$$$

Lean4

@[simp]
theorem map_rTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) (x : S ⊗[R] N) :
    map f g (f'.rTensor _ x) = map (f.comp f') g x :=
  LinearMap.congr_fun (map_comp_rTensor _ _ _ _) x

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