map_comp_rTensor — Mathlib

English

A relation between two tensor constructions: (lTensor P g).comp (rTensor N f) equals TensorProduct.map f g.

Русский

Связь между двумя тензорными конструкциями: (lTensor P g).comp (rTensor N f) эквивалентно TensorProduct.map f g.

LaTeX

$$$(\,\mathrm{lTensor}\ P\ g).\mathrm{comp} (\mathrm{rTensor}\ N\ f) = \mathrm{TensorProduct}.map f g$$$

Lean4

@[simp]
theorem map_comp_rTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) :
    (map f g).comp (f'.rTensor _) = map (f.comp f') g := by simp only [rTensor, ← map_comp, comp_id]

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