lTensor_comp_rTensor — Mathlib

English

Left-tensorization preserves multiplication of endomorphisms: (f * g).lTensor M = f.lTensor M * g.lTensor M.

Русский

Левотензоризация сохраняет умножение эндоморфизмов: (f * g).lTensor M = f.lTensor M * g.lTensor M.

LaTeX

$$$(f * g).lTensor M = f.lTensor M \circ g.lTensor M$$$

Lean4

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

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